Alphabeta Math
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 14 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 11 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Riemann Mapping Theorem

1 · Prerequisites

2 · Summary

This page gives the classical extremal proof of the Riemann mapping theorem in the four auditable stages fixed by the design: build a nonempty normalized competitor family, show its derivative supremum is finite and attained, prove the extremal limit remains univalent, and then enlarge any proper image of the disc to contradict extremality. The resulting map is the normalized conformal equivalence from a proper homologically simply connected plane domain to the unit disc.

The second half records the standard univalent-function consequences used throughout the subject. The area theorem yields the sharp second-coefficient bound, which in turn gives Koebe's quarter theorem, the sharp derivative distortion estimate, both sharp growth estimates, and the local quarter-disc inclusion for arbitrary univalent disc maps.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-30Open item page →

Univalent holomorphic functions

Definition

Let Ω be a complex domain. A holomorphic function f:Ω→C is univalent when it is injective.

Thus "univalent" on a plane domain means exactly "one-to-one and holomorphic" on that domain.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-30Open item page →

The normalized univalent class on the unit disc

Definition

The normalized univalent class is

S:={ f:D→C:f is holomorphic and univalent, f(0)=0, f′(0)=1 },

where univalence is that of Univalent holomorphic functions.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-30Open item page →

The extremal family of disc-valued univalent maps fixing a basepoint

Definition

Let Ω⊊C be a homologically simply connected complex domain and let z0∈Ω. The Riemann extremal family at z0 is

F(Ω,z0):={ f:Ω→D:f is holomorphic and univalent, f(z0)=0, f′(z0)>0 }.

The derivative condition fixes the rotational ambiguity after the basepoint normalization.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30Open item page →

A proper homologically simply connected plane domain has a bounded univalent competitor

Statement

Let Ω⊊C be homologically simply connected and let z0∈Ω. Then the extremal family F(Ω,z0) is nonempty.

Facts & Assumptions

Given: A proper homologically simply connected complex domain Ω⊊C and a point z0∈Ω.

[L1]

On a homologically simply connected complex domain, every holomorphic nowhere-zero function has a holomorphic square root (A nonvanishing holomorphic function on such a domain has holomorphic roots of every positive order).

[L2]

For each a∈D, the Blaschke factor φa is a biholomorphic self-map of D (Blaschke factors are automorphisms of the disc).

[L3]

A nonconstant holomorphic map on a domain has open image (Open mapping theorem for holomorphic functions).

Proof

technique · direct
1.1L1givenchoose

Because Ω⊊C, choose a∈C∖Ω. The function z↦z−a is holomorphic and nowhere zero on Ω, so [L1] gives a holomorphic q:Ω→C with q(z)2=z−a.

2.1step 1.1algebra

If q(z1)=q(z2) then z1−a=q(z1)2=q(z2)2=z2−a, so z1=z2; thus q is injective. Also 0∉q(Ω), and q(Ω)∩(−q(Ω))=∅ because q(z1)=−q(z2) would again force z1=z2, hence q(z1)=0, impossible.

3.1L3step 2.1choose

Put w0:=q(z0). Since q is nonconstant, [L3] makes q(Ω) open, so choose ρ>0 with D(w0,ρ)⊆q(Ω). Step 2.1 gives q(Ω)∩(−q(Ω))=∅, hence D(−w0,ρ)=−D(w0,ρ)⊆−q(Ω) is disjoint from q(Ω). Therefore ∣q(z)+w0∣≥ρ for every z∈Ω.

4.1step 2.1step 3.1algebra

Define h(z):=ρ2(q(z)+w0). Step 3.1 gives ∣h(z)∣≤1/2, so h(Ω)⊆D. The reciprocal affine map is injective away from −w0, and step 2.1 makes q injective, so h is holomorphic and injective on Ω.

5.1L2step 1.1step 4.1algebra∎

Let b=h(z0)∈D. By [L2], g:=φb∘h is holomorphic and injective from Ω into D, and g(z0)=0. Differentiating q2=z−a gives q′(z0)=1/(2w0)≠0, so g′(z0)≠0. Multiplying by the unimodular constant g′(z0)‾/∣g′(z0)∣ makes the derivative at z0 positive. The resulting map lies in F(Ω,z0).

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

The extremal derivatives are positive and have a finite supremum

Statement

Let Ω⊊C be homologically simply connected and let z0∈Ω. Then the set

E:={ f′(z0):f∈F(Ω,z0) }

is a nonempty subset of (0,∞) with finite supremum.

Facts & Assumptions

Given: A proper homologically simply connected complex domain Ω⊊C and z0∈Ω.

[L1]
[L2]

Every f∈F(Ω,z0) satisfies f(z0)=0 and f′(z0)>0 (The extremal family of disc-valued univalent maps fixing a basepoint).

[L3]

Cauchy estimates bound derivatives from a modulus bound on a larger concentric circle (Cauchy estimates on a smaller concentric disc).

Proof

technique · direct
1.1L1L2given

Fact [L1] gives at least one map in F(Ω,z0), so the derivative set E is nonempty. Fact [L2] makes every element of E strictly positive.

1.2L2L3givenchoose

Choose ρ>0 with D(z0,ρ)‾⊂Ω. If f∈F(Ω,z0), then ∣f∣≤1 on D(z0,ρ) because f(Ω)⊂D, so [L3] gives ∣f′(z0)∣≤1/ρ. Since [L2] makes f′(z0) positive real, this is the same as f′(z0)≤1/ρ.

2.1step 1.1step 1.2∎

Therefore E⊂(0,1/ρ], so E has a finite supremum.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

A maximizing sequence has a locally uniform limit with extremal derivative

Statement

Assume the Axiom of Choice. Let Ω⊊C be homologically simply connected, let z0∈Ω, and let

M:=sup⁡{ f′(z0):f∈F(Ω,z0) }.

Then there is a holomorphic f:Ω→D with f(z0)=0 and f′(z0)=M.

Facts & Assumptions

Given: The Axiom of Choice, a proper homologically simply connected complex domain Ω⊊C, and a point z0∈Ω.

[A1]

The Axiom of Choice supplies the maximizing sequence and the successive subsequence choices used by Montel's theorem (The Axiom of Choice).

[L1]

The derivative set of the extremal family is nonempty, positive, and has a finite supremum (The extremal derivatives are positive and have a finite supremum).

[L2]

Under the Axiom of Choice, every locally bounded holomorphic family is normal (Montel's theorem: every locally bounded holomorphic family is normal).

[L3]

Derivatives depend continuously on locally uniform convergence (Every derivative operator is continuous for locally uniform convergence on holomorphic functions).

[L4]

A nonconstant holomorphic map on a complex domain is open (Open mapping theorem for holomorphic functions).

Proof

technique · direct
1.1A1L1L2givenchoose

By [A1] and [L1], choose a sequence (fn) in F(Ω,z0) with fn′(z0)→M. Because every fn maps Ω into D, the family is locally bounded, so [L2] gives a locally uniformly convergent subsequence, still denoted (fn), with holomorphic limit f on Ω.

2.1L3step 1.1algebra

For every n, one has fn(z0)=0, so the locally uniform convergence of step 1.1 gives f(z0)=0. Fact [L3] gives fn′(z0)→f′(z0), hence f′(z0)=M.

3.1L1L4step 2.1assume-contradischarge-contradiction

Because M>0 by [L1], step 2.1 makes f nonconstant. Also ∣f∣≤1 on Ω as a locally uniform limit of disc-valued maps. If ∣f(a)∣=1 at some a∈Ω, then f(Ω) would be an open subset of the closed unit disc by [L4], impossible. Hence f(Ω)⊂D.

4.1step 2.1step 3.1∎

The map f therefore has the required normalization and extremal derivative.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

A nonconstant locally uniform limit of univalent functions is univalent

Statement

Let Ω be a complex domain, let fn:Ω→C be univalent for every n, and suppose fn→f locally uniformly on Ω. If f is nonconstant, then f is univalent.

Facts & Assumptions

Given: A complex domain Ω, univalent maps fn:Ω→C, and locally uniform convergence fn→f to a nonconstant holomorphic limit.

[L1]

A univalent map is injective (Univalent holomorphic functions).

[L2]

A locally uniform limit of nowhere-zero holomorphic functions is either identically zero or nowhere zero (Hurwitz's zero-free limit theorem).

Proof

technique · direct
1.1L1givenalgebra

Fix a∈Ω. For each n, define hn(z):=fn(z)−fn(a)z−a(z∈Ω∖{a}). Since each fn is injective by [L1], the function hn has no zeros on Ω∖{a}. The removable singularity at a is filled by hn(a):=fn′(a), so each hn is holomorphic and nowhere zero on Ω.

2.1L2step 1.1algebra

The functions hn converge locally uniformly to h(z):={f(z)−f(a)z−a,z≠a,f′(a),z=a, because fn→f locally uniformly and derivatives converge locally uniformly as well. Fact [L2] therefore makes h either identically zero or nowhere zero.

3.1L1step 2.1discharge-construct∎

Since f is nonconstant, the function h is not identically zero. Hence step 2.1 makes h nowhere zero. If f(z)=f(a), then h(z)=0 unless z=a, so necessarily z=a. As a was arbitrary, f is injective and therefore univalent by [L1].

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

The extremal limit is univalent

Statement

In the setting of the extremal problem, any holomorphic limit attaining the supremal derivative is univalent.

Facts & Assumptions

Given: A locally uniformly convergent maximizing subsequence from the extremal family, with limit f.

[L1]

The limit f satisfies f′(z0)=M>0 (A maximizing sequence has a locally uniform limit with extremal derivative).

[L2]

A nonconstant locally uniform limit of univalent functions is univalent (A nonconstant locally uniform limit of univalent functions is univalent).

Proof

technique · direct
1.1L1given

By [L1], the derivative of f at the basepoint is positive, so f is nonconstant.

2.1L2step 1.1given∎

The maximizing sequence consists of univalent maps, so [L2] applies to the local uniform convergence in the given data. Together with step 1.1 it yields that f is univalent.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

An extremizer onto a proper subdomain of the disc can be enlarged

Statement

Let Ω⊊C be homologically simply connected, let z0∈Ω, and let f∈F(Ω,z0) attain the extremal derivative M. Then f(Ω)=D.

Facts & Assumptions

Given: A proper homologically simply connected complex domain Ω⊊C, a point z0∈Ω, and an extremizer f∈F(Ω,z0) with f′(z0)=M.

[L1]

The map f is univalent (The extremal limit is univalent).

[L2]

For each c∈D, the Blaschke factor φc is a disc automorphism (Blaschke factors are automorphisms of the disc).

[L3]

On a homologically simply connected complex domain, every holomorphic nowhere-zero function has a holomorphic square root (A nonvanishing holomorphic function on such a domain has holomorphic roots of every positive order).

Proof

technique · direct
1.1L1L2givenassume-contrachoose

Assume toward a contradiction that f(Ω)⊊D. Choose c∈D∖f(Ω). Since f(z0)=0, one has c≠0. Put β:=φc∘f. Then [L2] makes β holomorphic and injective into D, with β(Ω)⊂D∖{0}.

2.1L1L3step 1.1algebra

By [L3], the nowhere-zero holomorphic function β has a holomorphic square root q on Ω with q2=β. If q(z1)=q(z2) then β(z1)=β(z2), so injectivity of β gives z1=z2. If q(z1)=−q(z2) then again β(z1)=β(z2), so z1=z2 and then q(z1)=0, impossible because β never vanishes. Hence q is injective.

3.1L2step 2.1construct

Let a:=q(z0), so a2=β(z0)=φc(0)=c. Define g:=φa∘q. Then [L2] makes g holomorphic and injective from Ω into D, with g(z0)=0. Thus after multiplying by a unimodular constant if needed, g is another competitor in F(Ω,z0).

4.1L2step 3.1algebradischarge-contradiction

Differentiate q2=β at z0 to obtain 2a q′(z0)=β′(z0)=φc′(0)f′(z0)=−(1−∣c∣2)M. Since φa′(a)=−1/(1−∣a∣2) and ∣a∣2=∣c∣, one gets ∣g′(z0)∣=1−∣c∣22∣a∣(1−∣a∣2)M=1+∣c∣2∣c∣M>M, because (1+∣c∣)/2>∣c∣ for 0<∣c∣<1. This contradicts the extremal definition of M.

5.1step 4.1∎

Therefore the assumption of step 1.1 is false, so f(Ω)=D.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

Every proper homologically simply connected plane domain is conformally equivalent to the unit disc

Statement

Assume the Axiom of Choice. Let Ω⊊C be a homologically simply connected complex domain and let z0∈Ω. Then there is a biholomorphic map f:Ω→D such that

f(z0)=0,f′(z0)>0.

Facts & Assumptions

Given: The Axiom of Choice, a proper homologically simply connected complex domain Ω⊊C, and a point z0∈Ω.

[A1]

The Axiom of Choice is used by the extremal-attainment lemma (The Axiom of Choice).

[L1]

Under the Axiom of Choice, the extremal family is nonempty and the supremal derivative is attained by a holomorphic map f:Ω→D (A proper homologically simply connected plane domain has a bounded univalent competitor, A maximizing sequence has a locally uniform limit with extremal derivative).

[L3]

An injective holomorphic map on a complex domain is biholomorphic onto its open image (An injective holomorphic map has no critical point and is biholomorphic onto its image).

Proof

technique · direct
1.1A1L1givenchoose

By [A1] and [L1], choose a holomorphic map f:Ω→D with f(z0)=0 and extremal derivative f′(z0)>0.

2.1L2L3step 1.1

Fact [L2] makes this map injective and gives f(Ω)=D. Since Ω is a complex domain by the given data, [L3] makes f biholomorphic onto its image, which is exactly D.

3.1step 1.1step 2.1∎

The map of step 2.1 has the required normalization, so it is the desired conformal equivalence.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

The normalized Riemann map is unique

Statement

Let Ω⊊C be homologically simply connected and let z0∈Ω. If f,g:Ω→D are biholomorphic and satisfy

f(z0)=g(z0)=0,f′(z0)>0,g′(z0)>0,

then f=g.

Facts & Assumptions

Given: Two normalized biholomorphisms f,g:Ω→D as in the statement.

[L2]

A holomorphic self-map of D fixing 0 is a rotation, and equality in Schwarz's lemma is exactly the rotational case (Schwarz lemma with the equality cases).

[L3]

Complex derivatives satisfy the chain rule (The chain rule for complex derivatives).

Proof

technique · direct
1.1L1L2given

The composite h:=g∘f−1 is a biholomorphic self-map of D, and h(0)=0 because both maps send z0 to 0. Thus [L2] gives h(ζ)=eiθζ for some real θ.

2.1L3step 1.1algebra

Differentiate the identity g=h∘f at z0. By [L3], g′(z0)=h′(0)f′(z0)=eiθf′(z0). Since both displayed derivatives in the statement are positive real numbers, eiθ=1.

3.1step 1.1step 2.1∎

Hence h is the identity on D, so g=h∘f=f.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

The area theorem for exterior univalent functions

Statement

Let

g(z)=1z+∑n≥1bnzn

be holomorphic and univalent on 0<∣z∣<1. Then

∑n≥1n∣bn∣2≤1.

Facts & Assumptions

Given: A holomorphic univalent function g(z)=z−1+∑n≥1bnzn on 0<∣z∣<1.

[L1]

Univalence means injectivity (Univalent holomorphic functions).

[L2]

The derivative of an injective holomorphic map on a domain never vanishes (An injective holomorphic map has no critical point and is biholomorphic onto its image).

[L4]

A supplied finite decomposition into regions bounded in both coordinate directions is a finite elementary Green region (Type I, Type II, and elementary regions for Green's theorem).

[L5]

For a finite elementary Green region, area is one half the positively oriented integral of x dy−y dx (Area of an elementary Green region as a boundary line integral).

Proof

technique · direct
1.1L1L2givenalgebra

Fix 0<r<1 and put γr(t):=g(reit). By [L1], γr is simple on [0,2π), and by [L2], γr′(t)=ireitg′(reit)≠0. Thus Γr:=γr([0,2π]) is a regular real-analytic simple closed curve. Since g(z)=z−1+O(z) near zero, the image g({0<∣z∣<r}) is the unbounded side of Γr; write Er for the bounded side. The parametrization γr is clockwise relative to Er.

2.1L3L4step 1.1construct

The real and imaginary coordinate functions of γr and their derivatives are real analytic. Neither coordinate derivative is identically zero, since a regular simple closed curve cannot lie in one vertical or horizontal line. By [L3], the zeros of each derivative are isolated; periodic real analyticity and compactness of the parameter circle make both zero sets finite. Subdivide at those finitely many critical parameters and at the finitely many intersections with their horizontal and vertical critical lines. The nonintersecting coordinate-monotone arcs then bound finitely many pieces, each describable both between two piecewise-C1 graphs in x and between two such graphs in y. These pieces have disjoint interiors and share complete oppositely oriented arcs, so they supply Er with a finite elementary Green decomposition in the sense of [L4].

3.1L5step 1.1step 2.1algebra

Apply [L5] to the decomposition in step 2.1 and reverse the clockwise orientation from step 1.1. Writing w=g(z) and using dw=g′(z) dz gives Area⁡(Er)=−12i∫∣z∣=rg(z)‾g′(z) dz.

4.1step 3.1algebra

On ∣z∣=r, one has z‾=r2/z, so g(z)‾=zr2+∑n≥1bn‾r2nzn. Multiplying by g′(z)=−1z2+∑n≥1nbnzn−1 and taking the contour integral leaves only the z−1 coefficient. Hence 12i∫∣z∣=rg(z)‾g′(z) dz=π ⁣(∑n≥1n∣bn∣2r2n−1r2).

5.1step 3.1step 4.1algebra∎

Combining steps 3.1 and 4.1 with Area⁡(Er)≥0 gives ∑n≥1n∣bn∣2r2n≤1r2. For every N, discard the nonnegative terms with n>N and let r↑1 to obtain ∑n=1Nn∣bn∣2≤1. Letting N→∞ proves the asserted inequality.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30Open item page →

The second coefficient of a normalized univalent function has modulus at most two

Statement

If

f(z)=z+a2z2+a3z3+⋯

lies in S, then ∣a2∣≤2.

Facts & Assumptions

Given: A function f(z)=z+a2z2+a3z3+⋯∈S.

[L1]

The area theorem applies to univalent functions of the form z−1+∑n≥1bnzn on the punctured disc (The area theorem for exterior univalent functions).

[L2]

The unit disc is star-shaped and therefore homologically simply connected (Star-shaped plane domains are homologically simply connected).

[L3]

A nowhere-zero holomorphic function on such a domain has a holomorphic square root (A nonvanishing holomorphic function on such a domain has holomorphic roots of every positive order).

Proof

technique · direct
1.1L2L3givenalgebra

Since f is injective and f(0)=0, the only zero of f in D is 0. Hence F(z):=f(z2)z2=1+a2z2+a3z4+⋯ extends holomorphically and nowhere vanishingly to D. By [L2] and [L3], choose a holomorphic square root q on D with q(z)2=F(z) and q(0)=1.

2.1step 1.1algebra

Put h(z):=zq(z). Then h(z)2=f(z2). The function h is odd and univalent: if h(z1)=h(z2) then f(z12)=f(z22), so z12=z22; if z1=−z2≠0, oddness gives h(z1)=−h(z2), contradiction. Thus h(z)=z+a22z3+⋯ .

3.1L1step 2.1algebra

Define G(ζ):=1h(ζ)=1ζ−a22ζ+⋯(0<∣ζ∣<1). Since h is injective on D and vanishes only at 0, the map G is holomorphic and injective on the punctured disc. Fact [L1] therefore applies and yields ∣a22∣2≤1.

4.1step 3.1∎

Therefore ∣a2∣≤2.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30Open item page →

Every normalized univalent disc map contains the quarter disc

Statement

If f∈S, then

D(0,1/4)⊂f(D).

Facts & Assumptions

Given: A function f∈S.

[L1]

Every normalized univalent function satisfies ∣a2∣≤2 (The second coefficient of a normalized univalent function has modulus at most two).

Proof

technique · direct
1.1L1givenassume-contraalgebra

Assume toward a contradiction that w∈C with 0<∣w∣<1/4 is omitted by f(D). Define g(z):=wf(z)w−f(z). Then g is holomorphic and univalent on D, g(0)=0, and g′(0)=1,g(z)=z+(a2+1w)z2+⋯ .

2.1L1step 1.1discharge-contradiction

Since g∈S, fact [L1] gives ∣a2+1w∣≤2. Applying [L1] again to f yields ∣a2∣≤2, so 1∣w∣≤∣a2+1w∣+∣a2∣≤4. Thus ∣w∣≥1/4, contradicting step 1.1.

3.1step 2.1∎

Therefore no value of modulus less than 1/4 is omitted, so D(0,1/4)⊂f(D).

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

Koebe's distortion theorem

Statement

If f∈S and ∣z∣=r<1, then

1−r(1+r)3≤∣f′(z)∣≤1+r(1−r)3.

Facts & Assumptions

Given: A function f∈S and a point z∈D with ∣z∣=r<1.

[L1]

For each a∈D, the Blaschke factor φa is a disc automorphism (Blaschke factors are automorphisms of the disc).

[L2]

If g(ζ)=ζ+Aζ2+⋯ lies in S, then ∣A∣≤2 (The second coefficient of a normalized univalent function has modulus at most two).

Proof

technique · direct
1.1L1givenalgebra

By rotating the source and target, it is enough to treat the case z=r∈[0,1). Define ψr(ζ):=ζ+r1+rζ,g(ζ):=f(ψr(ζ))−f(r)(1−r2)f′(r). Fact [L1] makes ψr an automorphism of D, so g∈S.

2.1L2step 1.1algebra

Differentiate twice at 0. Since ψr′(0)=1−r2 and ψr′′(0)=−2r(1−r2), one gets g′′(0)=(1−r2)f′′(r)f′(r)−2r. Because g∈S, [L2] gives ∣g′′(0)∣≤4. Therefore ∣f′′(r)f′(r)−2r1−r2∣≤41−r2.

3.1step 2.1algebra

Put H(r):=log⁡ ⁣((1−r2)f′(r)), choosing a continuous branch along [0,r] since f′ never vanishes on D for univalent f. Then step 2.1 yields ∣H′(t)∣=∣f′′(t)f′(t)−2t1−t2∣≤41−t2(0≤t<1).

4.1step 3.1algebra

Integrating step 3.1 from 0 to r and using f′(0)=1 gives ∣H(r)∣≤∫0r41−t2 dt=2log⁡1+r1−r. Exponentiating and dividing by 1−r2 yields 1−r(1+r)3≤∣f′(r)∣≤1+r(1−r)3.

5.1step 1.1step 4.1∎

The argument of steps 1.1 through 4.1 applies after rotation to every point of modulus r, so the same bounds hold for the original z.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

Koebe's growth theorem

Statement

If f∈S and ∣z∣=r<1, then

r(1+r)2≤∣f(z)∣≤r(1−r)2.

Facts & Assumptions

Given: A function f∈S and a point z∈D with ∣z∣=r<1.

[L1]

Koebe's distortion theorem gives 1−∣ζ∣(1+∣ζ∣)3≤∣f′(ζ)∣≤1+∣ζ∣(1−∣ζ∣)3(ζ∈D) for every f∈S (Koebe's distortion theorem).

Proof

technique · direct
1.1givenalgebra

Write z=reiθ. Since f(0)=0, f(z)=∫0reiθf′(teiθ) dt. Therefore ∣f(z)∣≤∫0r∣f′(teiθ)∣ dt.

1.2givenchoosealgebra

For the lower bound, choose z0 on ∣z∣=r for which ∣f(z0)∣ is minimal. The segment from 0 to f(z0) lies in f(D(0,r)‾): otherwise its first exit point from f(D(0,r)) would be an image of the circle ∣z∣=r having modulus strictly smaller than ∣f(z0)∣. Since f is univalent, this segment has a lift γ from 0 to z0.

2.1L1step 1.1algebra

Applying [L1] inside the integral gives ∣f(z)∣≤∫0r1+t(1−t)3 dt=r(1−r)2.

2.2L1step 1.2algebra

The image of γ is a straight segment, so [L1] gives ∣f(z0)∣=∫γ∣f′(ζ)∣ ∣dζ∣≥∫γ1−∣ζ∣(1+∣ζ∣)3 ∣dζ∣≥∫0r1−t(1+t)3 dt=r(1+r)2. The penultimate inequality follows because γ joins radius 0 to radius r, while the integrand is positive and depends only on the radius.

3.1step 2.1step 2.2∎

Minimality of z0 now gives ∣f(z)∣≥∣f(z0)∣≥r/(1+r)2 for every ∣z∣=r. Together with step 2.1 this proves both bounds.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30Open item page →

A quarter-disc inclusion at every point of a univalent disc map

Statement

Let f:D→C be holomorphic and univalent, and let a∈D. Then

D ⁣(f(a),(1−∣a∣2)∣f′(a)∣4)⊂f(D).

Facts & Assumptions

Given: A holomorphic univalent map f:D→C and a point a∈D.

[L1]

For each a∈D, the Blaschke factor φa is a disc automorphism (Blaschke factors are automorphisms of the disc).

[L2]

Every normalized univalent disc map contains the quarter disc (Every normalized univalent disc map contains the quarter disc).

Proof

technique · direct
1.1L1givenalgebra

Define g(ζ):=f(φa(ζ))−f(a)−(1−∣a∣2)f′(a). By [L1], the map φa is an automorphism of D with φa(0)=a and φa′(0)=−(1−∣a∣2), so g is holomorphic and univalent on D, with g(0)=0 and g′(0)=1.

2.1L2step 1.1algebra∎

Thus g∈S, and [L2] gives D(0,1/4)⊂g(D). Multiplying by the affine factor from step 1.1 and translating back yields D ⁣(f(a),(1−∣a∣2)∣f′(a)∣4)⊂f(D).

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-30Open item page →

Choice strength used in the extremal proof of the Riemann mapping theorem

The displayed extremal proof assumes the Axiom of Choice. Its nonconstructive step is concentrated in the choice of a maximizing sequence and the successive subsequence extraction used in Montel's theorem. That is exactly the step isolated in A maximizing sequence has a locally uniform limit with extremal derivative and in the proof of Montel's theorem: every locally bounded holomorphic family is normal; once the limiting extremizer exists, the remaining univalence and surjectivity arguments are explicit.

5 · Examples, counterexamples and false statements

None yet.

Sources