Bloch.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

17 declarations, 7 contain sorry, 0 declared as axioms

Bloch and Landau constants

References:

Wikipedia
[CP96] Chen, H., Gauthier, P. M. "On Bloch's constant." Journal d'Analyse Mathématique 69 (1996), 275–291.
[AG37] Ahlfors, L. V., Grunsky, H. "Über die Blochsche Konstante." Mathematische Zeitschrift 42 (1937), 671–673.
[Ya95] Yanagihara, H. "On the locally univalent Bloch constant." Journal d'Analyse Mathématique 65 (1995), 1–17.
[Ra43] Rademacher, H. "On the Bloch-Landau Constant."" American Journal of Mathematics 65 (1943), 387–390.
OptimizationConstants
[Skin2009] Skinner, Brian. The univalent Bloch constant problem. Complex Variables and Elliptic Equations 54 (2009), no. 10, 951–955.
MathWorld
Bhowmik–Sen
[Re2008] Rettinger, R. "Bloch's constant is computable." Journal of Universal Computer Science 14 (2008), 896–907. In particular, a schlicht disk is the image of a subdomain under a biholomorphic restriction.

Imports (1)

FormalConjecturesUtil

def Bloch.blochRadius The Bloch radius line 55 source
Source documentation
The Bloch radius $B_f$ of a function $f$ is the supremum of radii of schlicht disks in the image of the unit disk under $f$: the restriction of f maps an open subdomain injectively and onto the disk. Requiring an open subdomain and equality of the image is essential; mere containment would allow an arbitrary set-theoretic choice of one preimage per point. Takes values in ℝ≥0∞ so that functions whose image contains arbitrarily large schlicht disks correctly get radius ⊤ rather than 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, ENNReal
Proof uses: SupSet.sSup, Set.image, Real, ENNReal.ofReal, Set.ofPred, Exists, Set, And, IsOpen, LE.le, Metric.ball, OfNat.ofNat, Eq, Set.InjOn
17 instances, coercions and auxiliary constants left out.
```
noncomputable def blochRadius (f : ℂ → ℂ) : ℝ≥0∞ :=
…
```
lemma Bloch.zero_le_blochRadius line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, LE.le, ENNReal, OfNat.ofNat, Bloch.blochRadius
Proof uses: zero_le
11 instances, coercions and auxiliary constants left out.
lemma Bloch.dis_add_radius_le_of_ball_subset_ball line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, NormedAddCommGroup, NormedSpace, Nontrivial, Real, LT.lt, OfNat.ofNat, LE.le, Set, Metric.ball, HAdd.hAdd, Dist.dist
Proof uses: Filter.Tendsto, nhdsWithin, Set.Iio, nhds, Filter.Tendsto.const_add, id, tendsto_nhds_of_tendsto_nhdsWithin, Filter.tendsto_id, le_of_tendsto, Filter.mp_mem, Set.Ioo, Set.ofPred, Ioo_mem_nhdsLT, Filter.univ_mem', Membership.mem, dite, Eq, Classical.propDecidable, Ne, Exists and 69 more
214 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma Bloch.radius_le_of_ball_subset_ball line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, NormedAddCommGroup, NormedSpace, Nontrivial, Real, LT.lt, OfNat.ofNat, LE.le, Set, Metric.ball
Proof uses: trans, HAdd.hAdd, Dist.dist, of_eq_true, Eq.trans, True, Bloch.dis_add_radius_le_of_ball_subset_ball
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Bloch.blochRadius_id_eq_one line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENNReal, Bloch.blochRadius, id, Complex, OfNat.ofNat
Proof uses: le_antisymm, sSup_le, Set.image, Real, ENNReal.ofReal, Set.ofPred, Exists, Set, And, IsOpen, LE.le, Metric.ball, Set.InjOn, Membership.mem, dite, LT.lt, LE.le.trans, ENNReal.ofReal_le_ofReal, Bloch.radius_le_of_ball_subset_ball, Eq.rec and 70 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
def Bloch.landauRadius The Landau radius $L_f$ of a function $f$ is the supremum of radii of disks contained in the image of the unit disk under $f$ line 123 source
Source documentation
The Landau radius $L_f$ of a function $f$ is the supremum of radii of disks contained in the image of the unit disk under $f$. Takes values in ℝ≥0∞ so that functions with unbounded image correctly get radius ⊤.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, ENNReal
Proof uses: SupSet.sSup, Set.image, Real, ENNReal.ofReal, Set.ofPred, Exists, LE.le, Set, Metric.ball, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.
```
noncomputable def landauRadius (f : ℂ → ℂ) : ℝ≥0∞ :=
…
```
def Bloch.blochConstant The Bloch constant $B$ is the largest radius such that every holomorphic function on the unit disk with $f'(0) = 1$ has a schlicht (univalent) disk of that radius in its image line 128 source
Source documentation
The Bloch constant $B$ is the largest radius such that every holomorphic function on the unit disk with $f'(0) = 1$ has a schlicht (univalent) disk of that radius in its image.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: SupSet.sSup, Set.ofPred, Complex, DifferentiableOn, Metric.ball, OfNat.ofNat, Eq, deriv, Exists, Set, And, IsOpen, LE.le, Set.image, Set.InjOn
23 instances, coercions and auxiliary constants left out.
```
noncomputable def blochConstant : ℝ :=
…
```
theorem Bloch.blochConstant_lower_bound It is proved in [CP96] that the Bloch constant is bounded below by $\sqrt{3}/4 + 2 \times 10^{-4}$ sorry line 135 source
Source documentation
It is proved in [CP96] that the Bloch constant is bounded below by $\sqrt{3}/4 + 2 \times 10^{-4}$

depends on sorry what this means
Statement uses: LE.le, Real, HAdd.hAdd, HDiv.hDiv, Real.sqrt, OfNat.ofNat, Nat, HMul.hMul, HPow.hPow, Int, Neg.neg, Bloch.blochConstant
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem blochConstant_lower_bound : Real.sqrt 3 / 4 + 2 * 10 ^ (-4 : ℤ) ≤ blochConstant := by
…
```
Mentions: Bloch.blochConstant
theorem Bloch.blochConstant_upper_bound It is proved in [AG37] that the Bloch constant is bounded above by $\frac{1}{\sqrt{1 + \sqrt{3}}}\frac{\Gamma(1/3) \Gamma(11/12)}{\Gamma(1/4)}$ sorry line 141 source
Source documentation
It is proved in [AG37] that the Bloch constant is bounded above by $\frac{1}{\sqrt{1 + \sqrt{3}}}\frac{\Gamma(1/3) \Gamma(11/12)}{\Gamma(1/4)}$.

depends on sorry what this means
Statement uses: LE.le, Real, Bloch.blochConstant, HDiv.hDiv, HMul.hMul, Real.Gamma, OfNat.ofNat, Nat, Real.sqrt, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem blochConstant_upper_bound :
    blochConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (11 / 12) /
    (Real.Gamma (1 / 4) * Real.sqrt (1 + Real.sqrt 3)) := by
…
```
Mentions: Bloch.blochConstant
theorem Bloch.blochConstant_exact_value Ahlfors and Grunsky also conjectured in [AG37] that this upper bound is the precise value of the Bloch constant sorry line 149 source
Source documentation
Ahlfors and Grunsky also conjectured in [AG37] that this upper bound is the precise value of the Bloch constant.

depends on sorry what this means
Statement uses: Eq, Real, Bloch.blochConstant, HDiv.hDiv, HMul.hMul, Real.Gamma, OfNat.ofNat, Nat, Real.sqrt, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem blochConstant_exact_value :
    blochConstant = Real.Gamma (1 / 3) * Real.Gamma (11 / 12) /
    (Real.Gamma (1 / 4) * Real.sqrt (1 + Real.sqrt 3)) := by
…
```
Mentions: Bloch.blochConstant
def Bloch.univalentBlochConstant The Univalent Bloch constant line 157 source
Source documentation
The Univalent Bloch constant $B_u$ is the largest radius such that every univalent holomorphic function on the unit disk with $f'(0) = 1$ has a schlicht disk of that radius in its image.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: SupSet.sSup, Set.ofPred, Complex, Set.InjOn, Metric.ball, OfNat.ofNat, DifferentiableOn, Eq, deriv, Exists, Set, And, IsOpen, LE.le, Set.image
23 instances, coercions and auxiliary constants left out.
```
noncomputable def univalentBlochConstant : ℝ :=
…
```
theorem Bloch.univalentBlochConstant_lower_bound It is proved in [Skin2009] that the Univalent Bloch constant is bounded below by $0.5708858$ sorry line 164 source
Source documentation
It is proved in [Skin2009] that the Univalent Bloch constant is bounded below by $0.5708858$.

depends on sorry what this means
Statement uses: LE.le, Real, OfScientific.ofScientific, Bool.true, Bloch.univalentBlochConstant
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem univalentBlochConstant_lower_bound : 0.5708858 ≤ univalentBlochConstant := by
…
```
Mentions: Bloch.univalentBlochConstant
theorem Bloch.univalentBlochConstant_upper_bound The Univalent Bloch constant is trivially bounded above by the Bloch radius of the identity function, which is $1$ line 170 source
Source documentation
The Univalent Bloch constant is trivially bounded above by the Bloch radius of the identity function, which is $1$. This is the best upper bound we know according to [OptimizationConstants].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LE.le, Real, Bloch.univalentBlochConstant, OfNat.ofNat
Proof uses: csSup_le, Set.ofPred, Complex, Set.InjOn, Metric.ball, DifferentiableOn, Eq, deriv, Exists, Set, And, IsOpen, Set.image, Exists.intro, Membership.mem, EmptyCollection.emptyCollection, And.intro, isOpen_empty, Set.empty_subset, of_eq_true and 72 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem univalentBlochConstant_upper_bound : univalentBlochConstant ≤ 1 := by
…
```
Mentions: Bloch.univalentBlochConstant
def Bloch.landauConstant The Landau constant $L$ is the largest radius such that every holomorphic function on the unit disk with $f'(0) = 1$ has a disk of that radius contained in its image line 185 source
Source documentation
The Landau constant $L$ is the largest radius such that every holomorphic function on the unit disk with $f'(0) = 1$ has a disk of that radius contained in its image.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: SupSet.sSup, Set.ofPred, Complex, DifferentiableOn, Metric.ball, OfNat.ofNat, Eq, deriv, Exists, LE.le, Set, Set.image
23 instances, coercions and auxiliary constants left out.
```
noncomputable def landauConstant : ℝ :=
…
```
theorem Bloch.landauConstant_lower_bound It is proved in [Ya95] that the Landau constant is bounded below by $0.5 + 10 ^ {-335}$ sorry line 191 source
Source documentation
It is proved in [Ya95] that the Landau constant is bounded below by $0.5 + 10 ^ {-335}$.

depends on sorry what this means
Statement uses: LE.le, Real, HAdd.hAdd, OfScientific.ofScientific, Bool.true, HPow.hPow, Int, OfNat.ofNat, Nat, Neg.neg, Bloch.landauConstant
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem landauConstant_lower_bound : 0.5 + 10 ^ (-335 : ℤ) ≤ landauConstant := by
…
```
Mentions: Bloch.landauConstant
theorem Bloch.landauConstant_upper_bound It is proved in [Ra43] that the Landau constant is bounded above by $\frac{1}{\sqrt{1 + \sqrt{3}}}\frac{\Gamma(1/3) \Gamma(5/6)}{\Gamma(1/6)}$ sorry line 197 source
Source documentation
It is proved in [Ra43] that the Landau constant is bounded above by $\frac{1}{\sqrt{1 + \sqrt{3}}}\frac{\Gamma(1/3) \Gamma(5/6)}{\Gamma(1/6)}$.

depends on sorry what this means
Statement uses: LE.le, Real, Bloch.landauConstant, HDiv.hDiv, HMul.hMul, Real.Gamma, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem landauConstant_upper_bound :
    landauConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6) := by
…
```
Mentions: Bloch.landauConstant
theorem Bloch.landauConstant_exact_value In [Ra43], Rademacher says that he strongly believed that this upper bound is the precise value of the Landau constant sorry line 204 source
Source documentation
In [Ra43], Rademacher says that he strongly believed that this upper bound is the precise value of the Landau constant.

depends on sorry what this means
Statement uses: Eq, Real, Bloch.landauConstant, HDiv.hDiv, HMul.hMul, Real.Gamma, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem landauConstant_exact_value :
    landauConstant = Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6) := by
…
```
Mentions: Bloch.landauConstant