Schwarz-Pick, Grönwall, Bierbach, Koebe

Stream: maths

[Geoffrey Irving]

I've proved a few more basic complex analysis results over the last while, but I don't think I've mentioned them here explicitly yet:

The Schwarz-Pick theorem, which is an easy corollary of Mathlib's Schwarz lemmas using Möbius transforms:

/-- Finite difference version of Schwarz-Pick for the unit disk -/
lemma Complex.dist_le_mul_mobius_of_mapsTo_unit_ball {f : ℂ → ℂ} (fa : ContDiffOn ℂ ω f (ball 0 1))
    (fi : MapsTo f (ball 0 1) (ball 0 1)) (z1 : ‖z‖ < 1) (w1 : ‖w‖ < 1) := ...

/-- Derivative version of Schwarz-Pick for the unit disk -/
lemma Complex.norm_deriv_le_div_of_mapsTo_unit_ball {f : ℂ → ℂ} (fa : ContDiffOn ℂ ω f (ball 0 1))
    (fi : MapsTo f (ball 0 1) (ball 0 1)) (z1 : ‖z‖ < 1) :
    ‖deriv f z‖ ≤ (1 - ‖f z‖ ^ 2) / (1 - ‖z‖ ^ 2) := ...

The Koebe quarter theorem, Bieberbach's coefficient inequality, and Grönwall's area theorem, which were more work:

/-- The Koebe quarter theorem, unit ball case -/
theorem koebe_quarter {f : ℂ → ℂ} (fa : AnalyticOnNhd ℂ f (ball 0 1)) (inj : InjOn f (ball 0 1)) :
    ball (f 0) (‖deriv f 0‖ / 4) ⊆ f '' (ball 0 1) := ...

theorem bieberbach {f : ℂ → ℂ} (fa : AnalyticOnNhd ℂ f (ball 0 1)) (inj : InjOn f (ball 0 1)) (f0 : f 0 = 0)
    (d0 : deriv f 0 = 1) : ‖deriv (deriv f) 0‖ ≤ 4 := ...

/-- The region strictly outside radius `r` -/
def norm_Ioi (r : ℝ) : Set ℂ := {w : ℂ | r < ‖w‖}

/-- The Grönwall area has a nice series-/
theorem gronwall_volume_sum {f : ℂ → ℂ} (fa : AnalyticOnNhd ℂ f (ball 0 1)) (f0 : f 0 = 1)
    (inj : InjOn (fun z ↦ z * f z⁻¹) (norm_Ioi 1)) :
    HasSum (fun n ↦ π * n * ‖iteratedDeriv (n + 1) f 0 / (n + 1).factorial‖ ^ 2)
      (π - volume.real ((fun z ↦ z * f z⁻¹) '' norm_Ioi 1)ᶜ) := ...

1. https://github.com/girving/ray/blob/main/Ray/Schwarz/SchwarzPick.lean
2. https://github.com/girving/ray/blob/main/Ray/Koebe/Koebe.lean
3. https://github.com/girving/ray/blob/main/Ray/Koebe/Bieberbach.lean
4. https://github.com/girving/ray/blob/main/Ray/Koebe/Gronwall.lean