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.
Schottky's theorem
Statement
For every and every there exists a constant such that every holomorphic map with satisfies
Facts & Assumptions
Given: Real numbers and , and a holomorphic map with .
The functions and admit holomorphic logarithms on (Disc functions omitting 0 and 1 admit holomorphic logarithms for f and 1-f).
The unit disc is homologically simply connected, so holomorphic roots and logs exist there for nowhere-zero functions (Star-shaped plane domains are homologically simply connected, A nonvanishing holomorphic function on such a domain has holomorphic roots of every positive order, A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm).
Bloch's theorem gives an absolute lower bound for normalized Bloch discs (Bloch's theorem).
The complex exponential satisfies (, and the complex exponential extends the real exponential) and is entire (The complex exponential is entire and its complex derivative is itself).
Proof
By [L1], choose with . Since omits , the function omits every integer. In particular and are nowhere zero, so [L2] gives holomorphic on with and . Then , so is nowhere zero, and [L2] gives a holomorphic with .
Using [L4] and , one gets and hence . Therefore , , and .
Put . First suppose . In step 1.1 choose the logarithm so that , which is possible because is determined up to an integer. Since , this also gives and hence for a fixed bound . Now and , so for one has . Because and , one also has . Finally choose the logarithm of so that ; then and therefore .
Let for , and set . If , then is an odd integer, so step 2.1 gives , impossible. Hence . The horizontal gaps between consecutive are less than , and the two vertical translates reduce the vertical gap to , so every open Euclidean disc of radius in meets .
Fix and rescale from the disc to the unit disc. If , then [L3] would produce a schlicht disc of radius greater than inside , contradicting step 3.1. Therefore for every .
If , integrate step 4.1 radially and use step 2.2 to get for . The formula in step 2.1 then bounds by a constant depending only on and . If , apply the same construction to : its center value lies between and , so the preceding case with center parameter uniformly bounds and hence . Taking the larger of the two bounds gives the required .
Depends on
- Disc functions omitting 0 and 1 admit holomorphic logarithms for f and 1-f
- Bloch's theorem
- A nonvanishing holomorphic function on such a domain has holomorphic roots of every positive order
- The complex exponential is entire and its complex derivative is itself
- $\exp(z+w)=\exp z\,\exp w$, and the complex exponential extends the real exponential
- Star-shaped plane domains are homologically simply connected
- A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm
Used by
Dependency tree · two levels
55 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
- Aleksander Simonic, The Ahlfors lemma and Picard's theorems, Theorem 11 (standard reference, not scraped)
- K. Stoll, Introductory Complex Analysis, Lemma 16.6 and Theorem 16.10 (standard reference, not scraped)