AI 中文总结
针对Σ类中凸函数的Pommerenke问题，研究人员构造了一个参数属于ℚ(i)的显式反例，证明Σ类中两个凸函数的凸线性组合未必为凸函数，且该论证已通过Lean 4形式化验证。
AI 中文摘要
设Σ表示在单位圆盘外部区域Δ^* = {z ∈ ℂ: |z| > 1}内解析且单叶的函数类，其形式为f(z) = z + b₀ + b₁z⁻¹ + …。1962年，Ch. Pommerenke证明：若F和G是Σ类中的凸函数，则其任意凸线性组合H = λF + (1−λ)G（0 < λ < 1）仍为单叶函数且属于Σ类。在Hayman的问题集《函数论研究问题》（问题6.10）中，Pommerenke提出疑问：H是否也必为凸函数？我们通过在Σ类中构造一个参数属于ℚ(i)的显式反例，以否定方式解决了该问题。该论证是自包含的，且已在Lean 4证明辅助工具中得到形式化验证。
英文摘要
Let $Σ$ denote the class of functions $f(z) = z + b_0 + b_1 z^{-1} + \cdots$ that are analytic and univalent in the exterior unit disk $Δ^* = \{z \in \mathbb{C} : |z| > 1\}$. In 1962, Ch. Pommerenke proved that if $F$ and $G$ are convex functions in $Σ$, then every convex linear combination $H = λF + (1-λ)G$ ($0 < λ< 1$) remains univalent and belongs to $Σ$. In Hayman's problem collection (Research Problems in Function Theory, Problem 6.10), Pommerenke raised the question of whether $H$ is necessarily also a convex function. We resolve this question in the negative by constructing an explicit counterexample in $Σ$ with parameters in $\mathbb{Q}(i)$. The argument is self-contained and has been formally certified in the Lean 4 proof assistant.
Comments6 pages, 1 table. Formal verification in Lean 4 available at https://github.com/Theophilus1030/Pommerenke
