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

noncomputable def Bloch.blochRadius (f : ℂ → ℂ) : ENNReal

The Bloch radius $B_f$ of a function $f$ is the supremum of radii of univalent disks in the image of the unit disk under $f$. Takes values in ℝ≥0∞ so that functions whose image contains arbitrarily large univalent disks correctly get radius ⊤ rather than 0.

Equations

• Bloch.blochRadius f = sSup (ENNReal.ofReal '' {r : ℝ | ∃ S ⊆ Metric.ball 0 1, ∃ (x : ℂ), Metric.ball x r ⊆ f '' S ∧ Set.InjOn f S})

theorem Bloch.zero_le_blochRadius (f : ℂ → ℂ) : 0 ≤ blochRadius f

theorem Bloch.dis_add_radius_le_of_ball_subset_ball {X : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [Nontrivial X] {x y : X} {r d : ℝ} (hpos : 0 < r) (hsub : Metric.ball x r ⊆ Metric.ball y d) : dist x y + r ≤ d

theorem Bloch.radius_le_of_ball_subset_ball {X : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [Nontrivial X] {x y : X} {r d : ℝ} (hpos : 0 < r) (hsub : Metric.ball x r ⊆ Metric.ball y d) : r ≤ d

theorem Bloch.blochRadius_id_eq_one : blochRadius id = 1

noncomputable def Bloch.landauRadius (f : ℂ → ℂ) : ENNReal

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 ⊤.

Equations

• Bloch.landauRadius f = sSup (ENNReal.ofReal '' {r : ℝ | ∃ (x : ℂ), Metric.ball x r ⊆ f '' Metric.ball 0 1})

noncomputable 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.

Equations

• One or more equations did not get rendered due to their size.

theorem Bloch.blochConstant_lower_bound : √3 / 4 + 2 * 10 ^ (-4) ≤ blochConstant

It is proved in [CP96] that the Bloch constant is bounded below by $\sqrt{3}/4 + 2 \times 10^{-4}$

theorem Bloch.blochConstant_upper_bound : blochConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (11 / 12) / (Real.Gamma (1 / 4) * √(1 + √3))

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)}$$.

theorem Bloch.blochConstant_exact_value : blochConstant = Real.Gamma (1 / 3) * Real.Gamma (11 / 12) / (Real.Gamma (1 / 4) * √(1 + √3))

Ahlfors and Grunsky also conjectured in [AG37] that this upper bound is the precise value of the Bloch constant.

noncomputable def Bloch.univalentBlochConstant : ℝ

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.

Equations

• One or more equations did not get rendered due to their size.

theorem Bloch.univalentBlochConstant_lower_bound : 0.5708858 ≤ univalentBlochConstant

It is proved in [Skin2009] that the Univalent Bloch constant is bounded below by $0.5708858$.

theorem Bloch.univalentBlochConstant_upper_bound : univalentBlochConstant ≤ 1

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].

noncomputable 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.

Equations

• Bloch.landauConstant = sSup {B : ℝ | ∀ (f : ℂ → ℂ), DifferentiableOn ℂ f (Metric.ball 0 1) → deriv f 0 = 1 → ∃ (x : ℂ), Metric.ball x B ⊆ f '' Metric.ball 0 1}

theorem Bloch.landauConstant_lower_bound : 0.5 + 10 ^ (-335) ≤ landauConstant

It is proved in [Ya95] that the Landau constant is bounded below by $0.5 + 10 ^ {-335}$.

theorem Bloch.landauConstant_upper_bound : landauConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6)

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)}$.

theorem Bloch.landauConstant_exact_value : landauConstant = Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6)

In [Ra43], Rademacher says that he strongly believed that this upper bound is the precise value of the Landau constant.