Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30
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.

Koebe's growth theorem

Statement

If fS and z=r<1, then

r(1+r)2f(z)r(1r)2.

Facts & Assumptions

Given: A function fS and a point zD with z=r<1.

[L1]

Koebe's distortion theorem gives 1ζ(1+ζ)3f(ζ)1+ζ(1ζ)3(ζD) for every fS (Koebe's distortion theorem).

Proof

technique · direct
1.1

Write z=reiθ. Since f(0)=0, f(z)=0reiθf(teiθ)dt. Therefore f(z)0rf(teiθ)dt.

givenalgebra
1.2

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.

givenchoosealgebra
2.1

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

L1step 1.1algebra
2.2

The image of γ is a straight segment, so [L1] gives f(z0)=γf(ζ)dζγ1ζ(1+ζ)3dζ0r1t(1+t)3dt=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.

L1step 1.2algebra
3.1

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.

step 2.1step 2.2

Depends on

Used by

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources