Papers With

← All papers
First page of A Counterexample to a Problem of Pommerenke on Convex Functions in the Class $Σ$

A Counterexample to a Problem of Pommerenke on Convex Functions in the Class $Σ$

Yuankai Guo, Xiaozhe Hu

math.CV Sep 3, 2026 · v1
formalization analysis
Read PDF arXiv abstract Code
TL;DR
A counterexample to Pommerenke's convexity problem in class Σ is formally certified in Lean 4 using Mathlib.
Abstract
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.
Problem

Pommerenke's Problem 6.10 asks whether a convex linear combination H = λF + (1-λ)G of convex functions F, G in the class Σ (univalent functions on the exterior unit disk) is necessarily convex. The problem had remained open with no reported progress.

Approach

Explicit convex functions F and G in Σ are constructed with parameters in the Gaussian rational field Q(i). A weighted Laurent-tail criterion establishes univalence of the combination H = (3/5)F + (2/5)G. The exterior convexity criterion is then evaluated at the rational test point z0 = 400/399 to show its failure. The complete argument—algebraic curvature certificate, branch-choice verification, residue vanishing, and univalence—is formalized in Lean 4 with Mathlib across 32 files ( 6,885 lines), with no extra axioms and no sorry/admit.

Results

The combination H is univalent and belongs to Σ but is not convex, resolving Pommerenke's question in the negative. The counterexample is fully machine-verified over Q(i) in Lean 4.

Paper StatementLean 4 TheoremSource File
Lemma 2.1alpha_normSq_lt_one, beta_normSq_lt_oneProblem610Counterexample.lean
Prop 2.2smoothExteriorConvexMap_FProblem610FGlobal.lean
Lemma 3.1injOn_of_hasInversePowerSeries_...ExteriorUnivalenceCriterion.lean
Theorem 1.2pommerenke_combination_not_convexMainTheorem.lean
Correspondence between paper results and formal Lean 4 theorems.