Prove the Schwarz-Pick theorem

This is the best bound on the derivative of a holomorphic function
within the ball, which we'll use to bound the derivative of bottcher in
terms of our bounds on its values.

Author: girving

Ray.lean

@@ -23,3 +23,5 @@ import Ray.Koebe.Koebe
 import Ray.Koebe.Wind
 import Ray.Koebe.WindArea
 import Ray.Misc.ChartedSpace
+import Ray.Schwarz.Mobius
+import Ray.Schwarz.SchwarzPick

Ray/Misc/Bound.lean

@@ -16,6 +16,10 @@ attribute [bound] norm_add_le mul_lt_of_lt_one_left Complex.normSq_nonneg norm_i
 
 @[bound] private alias ⟨_, Bound.ennreal_coe_pos⟩ := ENNReal.coe_pos
 
+@[bound] private alias ⟨_, Bound.sq_lt_one₀⟩ := sq_lt_one_iff₀
+
+@[bound] private alias ⟨_, Bound.sq_le_one₀⟩ := sq_le_one_iff₀
+
 @[bound] private lemma Bound.lt_mul_of_one_lt_left [MulOneClass α] [Zero α] {a b : α} [Preorder α]
     [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) (b1 : 1 < b) : a < b * a :=
   (lt_mul_iff_one_lt_left a0).mpr b1

Ray/Schwarz/Mobius.lean

@@ -0,0 +1,81 @@
+import Mathlib.Analysis.Calculus.ContDiff.Operations
+import Ray.Misc.Bound
+
+/-!
+## Facts about Möbius transforms
+
+We consider only Möbius transform of the form `z ↦ (w - z) / (1 - conj w * z)`, which is what we
+need to prove the Schwarz-Pick theorem.
+-/
+
+open Metric (ball)
+open Set
+open scoped ComplexConjugate ContDiff Topology
+noncomputable section
+
+variable {w z : ℂ}
+
+/-- The particular Möbius transform we need for Schwarz-Pick -/
+def mobius (w z : ℂ) : ℂ :=
+  (w - z) / (1 - conj w * z)
+
+/-- As a definition, for simp convenience -/
+lemma mobius_def (w z : ℂ) : mobius w z = (w - z) / (1 - conj w * z) := rfl
+
+/-- Our Möbius denominator is nonsingular -/
+lemma norm_mobius_denom_pos (w1 : ‖w‖ < 1) (z1 : ‖z‖ < 1) : 0 < ‖1 - conj w * z‖ := by
+  calc ‖1 - conj w * z‖
+    _ ≥ ‖(1 : ℂ)‖ - ‖conj w * z‖ := by bound
+    _ = 1 - ‖w‖ * ‖z‖ := by simp
+    _ ≥ 1 - ‖z‖ := by bound
+    _ > 0 := by linarith
+
+/-- Our Möbius denominator is nonsingular -/
+lemma mobius_denom_ne_zero (w1 : ‖w‖ < 1) (z1 : ‖z‖ < 1) : 1 - conj w * z ≠ 0 :=
+  norm_pos_iff.mp (norm_mobius_denom_pos w1 z1)
+
+/-- Our Möbius transforms map the unit disk to itself -/
+lemma mapsTo_mobius (w1 : ‖w‖ < 1) : MapsTo (mobius w) (ball 0 1) (ball 0 1) := by
+  intro z z1
+  simp only [Metric.mem_ball, dist_zero_right] at z1
+  simp only [Metric.mem_ball, dist_zero_right, mobius, Complex.norm_div,
+    div_lt_iff₀ (norm_mobius_denom_pos w1 z1), one_mul]
+  rw [← sq_lt_sq₀ (by bound) (by bound), ← Complex.ofReal_re (‖w - z‖ ^ 2),
+    ← Complex.ofReal_re (‖1 - (starRingEnd ℂ) w * z‖ ^ 2)]
+  simp only [← Complex.conj_mul', Complex.ofReal_pow, map_sub, mul_sub, sub_mul, Complex.sub_re,
+    mul_one, map_one, Complex.one_re, Complex.conj_conj, map_mul, one_mul]
+  rw [← sub_pos]
+  ring_nf
+  refine lt_of_lt_of_le (b := (1 - ‖w‖ ^ 2 : ℂ).re * (1 - ‖z‖ ^ 2 : ℂ).re) ?_ (le_of_eq ?_)
+  · simp only [Complex.ofReal_re, ← Complex.ofReal_pow, Complex.sub_re, Complex.one_re]
+    bound
+  · simp only [Complex.conj_mul', ← mul_assoc, mul_comm _ (conj w)]
+    simp only [mul_assoc, Complex.conj_mul', Complex.sub_re, Complex.one_re, ← Complex.ofReal_pow,
+      Complex.ofReal_re, ← Complex.ofReal_mul]
+    ring
+
+/-- Our Möbius transforms are analytic -/
+lemma contDiffAt_mobius {n : WithTop ℕ∞} (w1 : ‖w‖ < 1) (z1 : ‖z‖ < 1) :
+    ContDiffAt ℂ n (mobius w) z := by
+  refine ContDiffAt.div (by fun_prop) (by fun_prop) ?_
+  exact mobius_denom_ne_zero w1 z1
+
+/-- Our Möbius transforms are analytic -/
+lemma contDiffOn_mobius {n : WithTop ℕ∞} (w1 : ‖w‖ < 1) : ContDiffOn ℂ n (mobius w) (ball 0 1) :=
+  fun z z1 ↦ (contDiffAt_mobius w1 (by simpa using z1)).contDiffWithinAt
+
+/-- Our Möbius transforms map the unit disk to itself -/
+lemma norm_mobius_lt_one (w1 : ‖w‖ < 1) (z1 : ‖z‖ < 1) : ‖mobius w z‖ < 1 := by
+  simpa using mapsTo_mobius w1 (x := z) (by simpa)
+
+/-- Our Möbius transforms are involutions -/
+lemma mobius_mobius (w1 : ‖w‖ < 1) (z1 : ‖z‖ < 1) : mobius w (mobius w z) = z := by
+  have n1 := mobius_denom_ne_zero w1 z1
+  have n2 := mobius_denom_ne_zero w1 (norm_mobius_lt_one w1 z1)
+  simp only [mobius] at n1 n2 ⊢
+  rw [div_eq_iff n2, ← mul_left_inj' n1]
+  simp only [sub_mul, div_mul_cancel₀ _ n1, mul_assoc]
+  ring
+
+@[simp] lemma mobius_zero : mobius w 0 = w := by simp [mobius]
+@[simp] lemma mobius_self : mobius w w = 0 := by simp [mobius]

Ray/Schwarz/SchwarzPick.lean

@@ -0,0 +1,66 @@
+import Mathlib.Analysis.Complex.Schwarz
+import Ray.Schwarz.Mobius
+
+/-!
+## Schwarz-Pick theorem
+
+The Schwarz-Pick theorem provides the tightest bounds on finite differences and derivatives of
+an anlytic function on the unit disk:
+
+  https://en.wikipedia.org/wiki/Schwarz_lemma#Schwarz%E2%80%93Pick_theorem
+-/
+
+open Filter (Tendsto)
+open Metric (ball isOpen_ball)
+open Set
+open scoped ComplexConjugate ContDiff Topology
+noncomputable section
+
+variable {w z : ℂ} {f : ℂ → ℂ}
+
+/-- Finite difference version of Schwarz-Pick for the unit disk -/
+lemma Complex.dist_le_mul_mobius_of_mapsTo_unit_ball (fa : ContDiffOn ℂ ω f (ball 0 1))
+    (fi : MapsTo f (ball 0 1) (ball 0 1)) (z1 : ‖z‖ < 1) (w1 : ‖w‖ < 1) :
+    ‖f z - f w‖ ≤ ‖1 - conj (f z) * f w‖ * ‖mobius z w‖ := by
+  have fz1 : ‖f z‖ < 1 := by simpa using fi (x := z) (by simpa)
+  have fw1 : ‖f w‖ < 1 := by simpa using fi (x := w) (by simpa)
+  set g := mobius (f z) ∘ f ∘ mobius z
+  have gm' := fi.comp (mapsTo_mobius z1)
+  have gm : MapsTo g (ball 0 1) (ball 0 1) := (mapsTo_mobius fz1).comp gm'
+  have ga : ContDiffOn ℂ ω g (ball 0 1) :=
+    (contDiffOn_mobius fz1).comp (fa.comp (contDiffOn_mobius z1) (mapsTo_mobius z1)) gm'
+  have g0 : g 0 = 0 := by simp only [g, Function.comp_apply, mobius_zero, mobius_self]
+  set u := mobius z w
+  have u1 : ‖u‖ < 1 := norm_mobius_lt_one z1 w1
+  simpa only [g, Function.comp_apply, mobius_def (f z), u, mobius_mobius z1 w1, norm_div,
+    div_le_iff₀ (norm_mobius_denom_pos fz1 fw1), mul_comm ‖mobius _ _‖] using
+    Complex.norm_le_norm_of_mapsTo_ball_self (ga.differentiableOn le_top) gm g0 u1
+
+/-- Derivative version of Schwarz-Pick for the unit disk -/
+lemma Complex.norm_deriv_le_div_of_mapsTo_unit_ball (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) := by
+  have zm : z ∈ ball 0 1 := by simpa using z1
+  have fz1 : ‖f z‖ < 1 := by simpa using fi (x := z) (by simpa)
+  have df := (fa.differentiableOn le_top).differentiableAt (x := z) (isOpen_ball.mem_nhds zm)
+  have s : ∀ᶠ w in 𝓝[≠] z, ‖slope f z w‖ - ‖1 - conj (f z) * f w‖ / ‖1 - conj z * w‖ ≤ 0 := by
+    simp only [eventually_nhdsWithin_iff, mem_compl_iff, mem_singleton_iff]
+    filter_upwards [isOpen_ball.eventually_mem zm] with w w1 wz
+    simp only [Metric.mem_ball, dist_zero_right] at w1
+    have s := Complex.dist_le_mul_mobius_of_mapsTo_unit_ball fa fi z1 w1
+    simp only [mobius, Complex.norm_div, ← mul_div_assoc, mul_div_right_comm] at s
+    rw [← div_le_iff₀ (norm_pos_iff.mpr (by grind))] at s
+    simpa [slope, ← div_eq_inv_mul, norm_sub_rev (f w), norm_sub_rev w]
+  have dc : ContinuousAt (fun w ↦ ‖1 - conj (f z) * f w‖ / ‖1 - conj z * w‖) z :=
+    ContinuousAt.div (by fun_prop) (by fun_prop) (norm_mobius_denom_pos z1 z1).ne'
+  have t1 := (continuous_norm.tendsto _).comp df.hasDerivAt.tendsto_slope
+  have t2 := dc.tendsto
+  have e : ∀ x : ℝ, (1 - x : ℂ) = (1 - x : ℝ) := by simp
+  have n : ∀ {z : ℂ}, ‖z‖ < 1 → |1 - ‖z‖ ^ 2| = (1 - ‖z‖ ^ 2) := by
+    intro z z1
+    rw [abs_of_nonneg]
+    bound
+  simp only [Function.comp_def, conj_mul', ← Complex.ofReal_pow, e, Complex.norm_real,
+    Real.norm_eq_abs, n z1, n fz1] at t1 t2
+  rw [← sub_nonpos]
+  exact le_of_tendsto (t1.sub (t2.mono_left nhdsWithin_le_nhds)) s