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.
-/
module

public 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

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

@[expose] public sectionopen scoped Topology ENNRealopen Metric Set Filternamespace Bloch

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.

noncomputable def blochRadius (f : ℂ → ℂ) : ℝ≥0∞ :=
  sSup (ENNReal.ofReal '' {r : ℝ | ∃ S, IsOpen S ∧ S ⊆ ball (0 : ℂ) 1 ∧
    ∃ x, f '' S = ball x r ∧ 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))⊢ 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))⊢ ∀ᶠ (c : ℝ) in 𝓝[<] r, dist x y + c ≤ d
  filter_upwards [Ioo_mem_nhdsLT hpos] with t ⟨hl, hr⟩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))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))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))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))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))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 ≤ dposX: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⊢ t ≤ d apply norm_smul_inv_normX: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 ≠ 0posX: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⊢ t ≤ d; grindposX: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⊢ t ≤ dposX: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⊢ t ≤ d
    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⊢ 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⊢ ‖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⊢ ‖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))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))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 ≤ 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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ dist x y + t ≤ d apply norm_smul_inv_normX: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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)⊢ x - y ≠ 0negX: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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ dist x y + t ≤ d; grindnegX: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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ 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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ dist x y + t ≤ d
    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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ dist x y + t = ‖x - y‖ + t
      simp [NormedAddCommGroup.dist_eq]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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖-x + y‖ = ‖x - y‖
      rw [← norm_neg (-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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖-(-x + y)‖ = ‖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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖-(-x + y)‖ = ‖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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖-(-x + y)‖ = ‖x - y‖
      simp [add_comm, sub_eq_add_neg]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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = ‖1 • (x - y) + (↑t * (↑‖x - y‖)⁻¹) • (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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = ‖1 • (x - y) + (↑t * (↑‖x - y‖)⁻¹) • (x - y)‖
      rw [← add_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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = ‖(1 + ↑t * (↑‖x - y‖)⁻¹) • (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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = ‖1 + ↑t * (↑‖x - y‖)⁻¹‖ * ‖x - y‖ norm_smulX: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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = ‖1 + ↑t * (↑‖x - y‖)⁻¹‖ * ‖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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = ‖1 + ↑t * (↑‖x - y‖)⁻¹‖ * ‖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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = |1 + t * ‖x - y‖⁻¹| * ‖x - y‖
      rw [abs_of_nonneg (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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ 0 ≤ 1 + t * ‖x - y‖⁻¹All goals completed! 🐙 positivityAll goals completed! 🐙All goals completed! 🐙), add_mul,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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = 1 * ‖x - y‖ + t * ‖x - y‖⁻¹ * ‖x - y‖All goals completed! 🐙 one_mul,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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = ‖x - y‖ + t * ‖x - y‖⁻¹ * ‖x - y‖All goals completed! 🐙 mul_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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = ‖x - y‖ + t * (‖x - y‖⁻¹ * ‖x - y‖)All goals completed! 🐙 inv_mul_cancel₀ (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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ ≠ 0All goals completed! 🐙 aesopAll goals completed! 🐙All goals completed! 🐙),
        mul_oneX: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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖x - y‖ + t = ‖x - y‖ + tAll goals completed! 🐙]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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖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))t:ℝhl:0 < thr:t < rhxy:x ≠ yu:X := (↑‖x - y‖)⁻¹ • (x - y)this:‖u‖ = 1⊢ ‖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⊢ ∀ b ∈ ENNReal.ofReal '' {r | ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, id '' S = ball x r ∧ InjOn id S}, b ≤ 1
    rintro _ ⟨r, ⟨S, -, hS, x, hball, -⟩, rfl⟩ar:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:id '' S = ball x r⊢ ENNReal.ofReal r ≤ 1
    simp only [image_id] at hballar:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x r⊢ ENNReal.ofReal r ≤ 1
    by_cases hpos : 0 < rposr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x rhpos:0 < r⊢ ENNReal.ofReal r ≤ 1negr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x rhpos:¬0 < r⊢ ENNReal.ofReal r ≤ 1
    ·posr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x rhpos:0 < r⊢ ENNReal.ofReal r ≤ 1 exact (ENNReal.ofReal_le_ofReal
        (radius_le_of_ball_subset_ball (𝕜 := ℂ) hpos (hball ▸ hS))).trans
        (byr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x rhpos:0 < r⊢ ENNReal.ofReal 1 ≤ 1 simp [ENNReal.ofReal_one]All goals completed! 🐙)
    ·negr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x rhpos:¬0 < r⊢ ENNReal.ofReal r ≤ 1 exact (ENNReal.ofReal_of_nonpos (byr:ℝS:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x rhpos:¬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⊢ 1 = ENNReal.ofReal 1a⊢ ENNReal.ofReal 1 ≤ blochRadius id simpAll goals completed! 🐙a⊢ ENNReal.ofReal 1 ≤ blochRadius id]a⊢ ENNReal.ofReal 1 ≤ blochRadius id
    exact le_sSup ⟨1, ⟨ball (0 : ℂ) 1, isOpen_ball, Subset.rfl, 0, by⊢ id '' ball 0 1 = 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, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ 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 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 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 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, IsOpen S ∧ S ⊆ ball 0 1 ∧
      ∃ x, f '' S = ball x B ∧ 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 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, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}.Nonemptyh₂⊢ ∀
  b ∈
    {B |
      ∀ (f : ℂ → ℂ),
        InjOn f (ball 0 1) →
          DifferentiableOn ℂ f (ball 0 1) →
            deriv f 0 = 1 → ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S},
  b ≤ 1
  ·h₁⊢ {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) →
          deriv f 0 = 1 → ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}.Nonempty -- the set is nonempty: 0 is in it (ball x 0 = ∅ ⊆ anything)
    exact ⟨0, fun f _ _ _ => ⟨∅, isOpen_empty, empty_subset _, 0, byf:ℂ → ℂx✝²:InjOn f (ball 0 1)x✝¹:DifferentiableOn ℂ f (ball 0 1)x✝:deriv f 0 = 1⊢ f '' ∅ = ball 0 0 ∧ InjOn f ∅ simpAll goals completed! 🐙⟩⟩
  ·h₂⊢ ∀
  b ∈
    {B |
      ∀ (f : ℂ → ℂ),
        InjOn f (ball 0 1) →
          DifferentiableOn ℂ f (ball 0 1) →
            deriv f 0 = 1 → ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ 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, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ 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, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}⊢ deriv id 0 = 1h₂B:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) →
          deriv f 0 = 1 → ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}h:∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, id '' S = ball x B ∧ InjOn id S⊢ B ≤ 1 simpAll goals completed! 🐙h₂B:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) →
          deriv f 0 = 1 → ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}h:∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, id '' S = ball x B ∧ InjOn id S⊢ B ≤ 1)h₂B:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) →
          deriv f 0 = 1 → ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}h:∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, id '' S = ball x B ∧ InjOn id S⊢ B ≤ 1
    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, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:id '' S = ball x B⊢ 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, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x B⊢ 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, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x Bhpos:0 < B⊢ B ≤ 1negB:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) →
          deriv f 0 = 1 → ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x Bhpos:¬0 < B⊢ B ≤ 1
    ·posB:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) →
          deriv f 0 = 1 → ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x Bhpos:0 < B⊢ B ≤ 1 exact radius_le_of_ball_subset_ball (𝕜 := ℂ) hpos (hball ▸ hS)All goals completed! 🐙
    ·negB:ℝhB:B ∈
  {B |
    ∀ (f : ℂ → ℂ),
      InjOn f (ball 0 1) →
        DifferentiableOn ℂ f (ball 0 1) →
          deriv f 0 = 1 → ∃ S, IsOpen S ∧ S ⊆ ball 0 1 ∧ ∃ x, f '' S = ball x B ∧ InjOn f S}S:Set ℂhS:S ⊆ ball 0 1x:ℂhball:S = ball x Bhpos:¬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 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 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 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