FormalConjectures.Wikipedia.Bloch

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

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

open scoped Topology ENNRealopen Metric Set Filternamespace Bloch

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.

noncomputable def blochRadius (f : ℂ → ℂ) : ℝ≥0∞ :=
  sSup (ENNReal.ofReal '' {r : ℝ | ∃ S ⊆ ball (0 : ℂ) 1, ∃ x, ball x r ⊆ f '' S ∧ InjOn f S})


@[category API, AMS 30]
lemma zero_le_blochRadius (f : ℂ → ℂ) : 0 ≤ blochRadius f := zero_le _


@[category API, AMS 54]
lemma dis_add_radius_le_of_ball_subset_ball {X 𝕜 : Type*} [RCLike 𝕜] [NormedAddCommGroup X]
    [NormedSpace 𝕜 X] [Nontrivial X] {x y : X} {r d : ℝ} (hpos : 0 < r) (hsub : ball x r ⊆ ball y d) :
    dist x y + r ≤ d := byX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y d⊢ dist x y + r ≤ d
  have : Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) :=
      (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id).const_add _X:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)⊢ dist x y + r ≤ d
  refine le_of_tendsto this ?_X:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)⊢ ∀ᶠ (c : ℝ) in 𝓝[<] r, dist x y + c ≤ d
  filter_upwards [Ioo_mem_nhdsLT hpos] with t ⟨hl, hr⟩hX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < r⊢ dist x y + t ≤ d
  by_cases! hxy : x = yposX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x = y⊢ dist x y + t ≤ dnegX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ y⊢ dist x y + t ≤ d
  ·posX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x = y⊢ dist x y + t ≤ d obtain ⟨v, hv⟩ := exists_ne (0 : X)posX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x = yv:Xhv:v ≠ 0⊢ dist x y + t ≤ d
    simp_all only [dist_self, zero_add]posX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rt:ℝv:Xhsub:ball y r ⊆ ball y dthis:Tendsto (fun s => s) (𝓝[<] r) (𝓝 r)hl:0 < thr:t < rhxy:x = yhv:v ≠ 0⊢ t ≤ d
    let u := (‖v‖⁻¹ : 𝕜) • vposX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rt:ℝv:Xhsub:ball y r ⊆ ball y dthis:Tendsto (fun s => s) (𝓝[<] r) (𝓝 r)hl:0 < thr:t < rhxy:x = yhv:v ≠ 0u:X := (↑‖v‖)⁻¹ • v⊢ t ≤ d
    have : ‖u‖ = 1 := byX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y d⊢ dist x y + r ≤ d apply norm_smul_inv_normhxX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rt:ℝv:Xhsub:ball y r ⊆ ball y dthis:Tendsto (fun s => s) (𝓝[<] r) (𝓝 r)hl:0 < thr:t < rhxy:x = yhv:v ≠ 0u:X := (↑‖v‖)⁻¹ • v⊢ v ≠ 0; grindAll goals completed! 🐙
    calc
    _ = ‖y + (t : 𝕜) • u - y‖ := byX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rt:ℝv:Xhsub:ball y r ⊆ ball y dthis✝:Tendsto (fun s => s) (𝓝[<] r) (𝓝 r)hl:0 < thr:t < rhxy:x = yhv:v ≠ 0u:X := (↑‖v‖)⁻¹ • vthis:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_1 v hv)⊢ t = ‖y + ↑t • u - y‖ simp_all [norm_smul, abs_of_nonneg hl.le]All goals completed! 🐙
    _ ≤ d := byX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rt:ℝv:Xhsub:ball y r ⊆ ball y dthis✝:Tendsto (fun s => s) (𝓝[<] r) (𝓝 r)hl:0 < thr:t < rhxy:x = yhv:v ≠ 0u:X := (↑‖v‖)⁻¹ • vthis:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_1 v hv)⊢ ‖y + ↑t • u - y‖ ≤ d
      refine (mem_ball_iff_norm.1 (hsub (mem_ball_iff_norm.2 ?_))).leX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rt:ℝv:Xhsub:ball y r ⊆ ball y dthis✝:Tendsto (fun s => s) (𝓝[<] r) (𝓝 r)hl:0 < thr:t < rhxy:x = yhv:v ≠ 0u:X := (↑‖v‖)⁻¹ • vthis:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_1 v hv)⊢ ‖y + ↑t • u - y‖ < r
      simp_all [norm_smul, abs_of_nonneg hl.le]All goals completed! 🐙
  ·negX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ y⊢ dist x y + t ≤ d let u := (‖x - y‖⁻¹ : 𝕜) • (x - y)negX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)⊢ dist x y + t ≤ d
    have : ‖u‖ = 1 := byX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y d⊢ dist x y + r ≤ d apply norm_smul_inv_normhxX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)⊢ x - y ≠ 0; grindAll goals completed! 🐙
    calc
    _ = ‖x - y‖ + t := byX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis✝:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_2 hxy)⊢ dist x y + t = ‖x - y‖ + t simp [NormedAddCommGroup.dist_eq]All goals completed! 🐙
    _ = ‖x + (t : 𝕜) • u - y‖ := byX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis✝:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_2 hxy)⊢ ‖x - y‖ + t = ‖x + ↑t • u - y‖
      simp [u, add_sub_right_comm, ← smul_assoc]X:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis✝:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_2 hxy)⊢ ‖x - y‖ + t = ‖x - y + (↑t * (↑‖x - y‖)⁻¹) • (x - y)‖
      nth_rw 2 [← one_smul 𝕜 (x - y)]X:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis✝:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_2 hxy)⊢ ‖x - y‖ + t = ‖1 • (x - y) + (↑t * (↑‖x - y‖)⁻¹) • (x - y)‖
      rw [← add_smul, norm_smul]X:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis✝:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_2 hxy)⊢ ‖x - y‖ + t = ‖1 + ↑t * (↑‖x - y‖)⁻¹‖ * ‖x - y‖
      norm_castX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis✝:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_2 hxy)⊢ ‖x - y‖ + t = |1 + t * ‖x - y‖⁻¹| * ‖x - y‖
      rw [abs_of_nonneg (by positivity), add_mul, one_mul, mul_assoc, inv_mul_cancel₀ (by aesop),
        mul_one]All goals completed! 🐙
    _ ≤ d := byX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis✝:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_2 hxy)⊢ ‖x + ↑t • u - y‖ ≤ d
      refine (mem_ball_iff_norm.1 (hsub (mem_ball_iff_norm.2 ?_))).leX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y dthis✝:Tendsto (fun s => dist x y + s) (𝓝[<] r) (𝓝 (dist x y + r)) := Tendsto.const_add (dist x y) (tendsto_nhds_of_tendsto_nhdsWithin tendsto_id)t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1 := norm_smul_inv_norm (dis_add_radius_le_of_ball_subset_ball._proof_2 hxy)⊢ ‖x + ↑t • u - x‖ < r
      simp_all [norm_smul, abs_of_nonneg hl.le]All goals completed! 🐙


@[category API, AMS 54]
lemma radius_le_of_ball_subset_ball {X 𝕜 : Type*} [RCLike 𝕜] [NormedAddCommGroup X]
    [NormedSpace 𝕜 X] [Nontrivial X] {x y : X} {r d : ℝ} (hpos : 0 < r)
    (hsub : ball x r ⊆ ball y d) : r ≤ d :=
  trans (byX:Type u_1𝕜:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace 𝕜 Xinst✝:Nontrivial Xx:Xy:Xr:ℝd:ℝhpos:0 < rhsub:ball x r ⊆ ball y d⊢ r ≤ dist x y + r simpAll goals completed! 🐙) (dis_add_radius_le_of_ball_subset_ball (𝕜 := 𝕜) hpos hsub)


@[category API, AMS 30]
lemma blochRadius_id_eq_one : blochRadius id = 1 := by⊢ blochRadius id = 1
  apply le_antisymma⊢ blochRadius id ≤ 1a⊢ 1 ≤ blochRadius id
  ·a⊢ blochRadius id ≤ 1 -- blochRadius id ≤ 1: every valid radius r satisfies r ≤ 1
    apply sSup_lea.a⊢ ∀ b ∈ ENNReal.ofReal '' {r | ∃ S ⊆ ball 0 1, ∃ x, ball x r ⊆ id '' S ∧ InjOn id S}, b ≤ 1
    rintro _ ⟨r, ⟨S, hS, x, hball, -⟩, rfl⟩a.ar:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x r ⊆ id '' S⊢ ENNReal.ofReal r ≤ 1
    simp only [image_id] at hballa.ar:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x r ⊆ S⊢ ENNReal.ofReal r ≤ 1
    by_cases hpos : 0 < rposr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x r ⊆ Shpos:0 < r⊢ ENNReal.ofReal r ≤ 1negr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x r ⊆ Shpos:¬0 < r⊢ ENNReal.ofReal r ≤ 1
    ·posr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x r ⊆ Shpos:0 < r⊢ ENNReal.ofReal r ≤ 1 exact (ENNReal.ofReal_le_ofReal
        (radius_le_of_ball_subset_ball (𝕜 := ℂ) hpos (hball.trans hS))).trans
        (byr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x r ⊆ Shpos:0 < r⊢ ENNReal.ofReal 1 ≤ 1 simp [ENNReal.ofReal_one]All goals completed! 🐙)
    ·negr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x r ⊆ Shpos:¬0 < r⊢ ENNReal.ofReal r ≤ 1 exact (ENNReal.ofReal_of_nonpos (byr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x r ⊆ Shpos:¬0 < r⊢ r ≤ 0 linarithAll goals completed! 🐙)).le.trans (zero_le _)
  ·a⊢ 1 ≤ blochRadius id -- 1 ≤ blochRadius id: ball 0 1 ⊆ id '' ball 0 1
    rw [show (1 : ℝ≥0∞) = ENNReal.ofReal 1 from by simp]a⊢ ENNReal.ofReal 1 ≤ blochRadius id
    exact le_sSup ⟨1, ⟨ball (0 : ℂ) 1, Subset.rfl, 0, by⊢ ball 0 1 ⊆ id '' ball 0 1 ∧ InjOn id (ball 0 1) simpAll goals completed! 🐙⟩, rfl⟩

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

noncomputable def landauRadius (f : ℂ → ℂ) : ℝ≥0∞ :=
  sSup (ENNReal.ofReal '' {r : ℝ | ∃ x, ball x r ⊆ f '' (ball (0 : ℂ) 1)})

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.

noncomputable def blochConstant : ℝ :=
  sSup {B : ℝ | ∀ f : ℂ → ℂ, DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 →
    ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}

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

@[category research solved, AMS 30]
theorem declaration uses 'sorry'blochConstant_lower_bound : Real.sqrt 3 / 4 + 2 * 10 ^ (-4 : ℤ) ≤ blochConstant := by⊢ √3 / 4 + 2 * 10 ^ (-4) ≤ blochConstant
  sorryAll goals completed! 🐙

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

@[category research solved, AMS 30]
theorem declaration uses 'sorry'blochConstant_upper_bound :
    blochConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (11 / 12) /
    (Real.Gamma (1 / 4) * Real.sqrt (1 + Real.sqrt 3)) := by⊢ blochConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (11 / 12) / (Real.Gamma (1 / 4) * √(1 + √3))
  sorryAll goals completed! 🐙

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

@[category research open, AMS 30]
theorem declaration uses 'sorry'blochConstant_exact_value :
    blochConstant = Real.Gamma (1 / 3) * Real.Gamma (11 / 12) /
    (Real.Gamma (1 / 4) * Real.sqrt (1 + Real.sqrt 3)) := by⊢ blochConstant = Real.Gamma (1 / 3) * Real.Gamma (11 / 12) / (Real.Gamma (1 / 4) * √(1 + √3))
  sorryAll goals completed! 🐙

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.

noncomputable def univalentBlochConstant : ℝ :=
  sSup {B : ℝ | ∀ f : ℂ → ℂ, InjOn f (ball 0 1) → DifferentiableOn ℂ f (ball 0 1) →
    deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}

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

@[category research solved, AMS 30]
theorem declaration uses 'sorry'univalentBlochConstant_lower_bound : 0.5708858 ≤ univalentBlochConstant := by⊢ 0.5708858 ≤ univalentBlochConstant
  sorryAll goals completed! 🐙

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

@[category research solved, AMS 30]
theorem univalentBlochConstant_upper_bound : univalentBlochConstant ≤ 1 := by⊢ univalentBlochConstant ≤ 1
  apply csSup_leh₁⊢ {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}.Nonemptyh₂⊢ ∀
  b ∈
    {B |
      ∀ (f : ℂ → ℂ),
        InjOn f (ball 0 1) →
          DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S},
  b ≤ 1
  ·h₁⊢ {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}.Nonempty -- the set is nonempty: 0 is in it (ball x 0 = ∅ ⊆ anything)
    exact ⟨0, fun f _ _ _ => ⟨∅, empty_subset _, 0, byf:ℂ → ℂx✝²:InjOn f (ball 0 1)x✝¹:DifferentiableOn ℂ f (ball 0 1)x✝:deriv f 0 = 1⊢ ball 0 0 ⊆ f '' ∅ ∧ InjOn f ∅ simpAll goals completed! 🐙⟩⟩
  ·h₂⊢ ∀
  b ∈
    {B |
      ∀ (f : ℂ → ℂ),
        InjOn f (ball 0 1) →
          DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S},
  b ≤ 1 -- every B in the set is ≤ 1
    intro B hBh₂B:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}⊢ B ≤ 1
    have h := hB id (injOn_id _) differentiableOn_id (byB:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}⊢ deriv id 0 = 1 simpAll goals completed! 🐙)
    rcases h with ⟨S, hS, x, hball, -⟩h₂B:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x B ⊆ id '' S⊢ B ≤ 1
    simp only [image_id] at hballh₂B:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x B ⊆ S⊢ B ≤ 1
    by_cases hpos : (0 : ℝ) < BposB:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x B ⊆ Shpos:0 < B⊢ B ≤ 1negB:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x B ⊆ Shpos:¬0 < B⊢ B ≤ 1
    ·posB:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x B ⊆ Shpos:0 < B⊢ B ≤ 1 exact radius_le_of_ball_subset_ball (𝕜 := ℂ) hpos (hball.trans hS)All goals completed! 🐙
    ·negB:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) → deriv f 0 = 1 → ∃ S ⊆ ball 0 1, ∃ x, ball x B ⊆ f '' S ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:ball x B ⊆ Shpos:¬0 < B⊢ B ≤ 1 linarithAll goals completed! 🐙

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.

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

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

@[category research solved, AMS 30]
theorem declaration uses 'sorry'landauConstant_lower_bound : 0.5 + 10 ^ (-335 : ℤ) ≤ landauConstant := by⊢ 0.5 + 10 ^ (-335) ≤ landauConstant
  sorryAll goals completed! 🐙

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

@[category research solved, AMS 30]
theorem declaration uses 'sorry'landauConstant_upper_bound :
    landauConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6) := by⊢ landauConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6)
  sorryAll goals completed! 🐙

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

@[category research open, AMS 30]
theorem declaration uses 'sorry'landauConstant_exact_value :
    landauConstant = Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6) := by⊢ landauConstant = Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6)
  sorryAll goals completed! 🐙


end Bloch