Various lemmas for needed by Koebe computations

Author: girving

Ray/Manifold/RiemannSphere.lean

@@ -97,6 +97,13 @@ public theorem continuousOn_toComplex : ContinuousOn OnePoint.toComplex ({∞}
   · simp only [mem_compl_iff, mem_singleton_iff, not_true] at m
   · exact continuousAt_toComplex.continuousWithinAt
 
+/-- `toComplex` is injective away from `∞` -/
+public lemma toComplex_inj {z w : 𝕊} (zi : z ≠ (∞ : 𝕊)) (wi : w ≠ (∞ : 𝕊)) :
+    z.toComplex = w.toComplex ↔ z = w := by
+  induction' z using OnePoint.rec
+  all_goals induction' w using OnePoint.rec
+  all_goals simp_all
+
 /-- Inversion in `𝕊`, interchanging `0` and `∞` -/
 public def inv (z : 𝕊) : 𝕊 := if z = 0 then ∞ else ↑z.toComplex⁻¹
 public instance : Inv 𝕊 := ⟨RiemannSphere.inv⟩

Ray/Multibrot/Basic.lean

@@ -394,7 +394,7 @@ theorem multibrot_eq_le_two :
     rcases(h 3).exists with ⟨n, h⟩; use n; linarith
 
 /-- `multibrot d` is compact -/
-theorem isCompact_multibrot : IsCompact (multibrot d) := by
+public theorem isCompact_multibrot : IsCompact (multibrot d) := by
   refine IsCompact.of_isClosed_subset (isCompact_closedBall _ _) ?_ multibrot_subset_closedBall
   rw [multibrot_eq_le_two]; apply isClosed_iInter; intro n
   refine IsClosed.preimage ?_ Metric.isClosed_closedBall
@@ -480,7 +480,7 @@ theorem bottcher_tendsto_zero : Tendsto (bottcher' d) (cobounded ℂ) (𝓝 0) :
   linarith
 
 /-- `bottcher' d` is analytic outside the Multibrot set -/
-theorem bottcher_analytic : AnalyticOnNhd ℂ (bottcher' d) (multibrot d)ᶜ := by
+public theorem bottcher_analytic : AnalyticOnNhd ℂ (bottcher' d) (multibrot d)ᶜ := by
   set s := superF d
   intro c m
   apply ContMDiffAt.analyticAt I I

Ray/Multibrot/Isomorphism.lean

@@ -160,6 +160,14 @@ public theorem bottcher_inj : InjOn (bottcher d) (multibrotExt d) := by
     rw [← norm_ne_zero_iff, norm_bottcher]
     linarith
 
+public lemma bottcher_inj' : InjOn (bottcher' d) (multibrot d)ᶜ := by
+  intro a am b bm e
+  simp only [mem_compl_iff, ← multibrotExt_coe] at am bm
+  simpa using bottcher_inj (d := d) am bm (by simp [bottcher, e])
+
+public lemma deriv_bottcher_ne_zero (m : c ∉ multibrot d) : deriv (bottcher' d) c ≠ 0 :=
+  bottcher_inj'.deriv_ne_zero isCompact_multibrot.isClosed.isOpen_compl m (bottcher_analytic _ m)
+
 /-!
 ## The external ray map, and `bottcherHomeomorph`
 -/

Ray/Schwarz/Mobius.lean

@@ -103,6 +103,17 @@ public lemma bijOn_mobius (w1 : ‖w‖ < 1) : BijOn (mobius w) (ball 0 1) (ball
 @[simp] public lemma mobius_zero : mobius w 0 = w := by simp [mobius]
 @[simp] public lemma mobius_self : mobius w w = 0 := by simp [mobius]
 
+public lemma mobius_eq_zero_iff (w1 : ‖w‖ < 1) (z1 : ‖z‖ < 1) :
+    mobius w z = 0 ↔ w = z := by
+  simp only [mobius, div_eq_zero_iff, sub_eq_zero, or_iff_left_iff_imp]
+  intro e
+  have lt : ‖conj w * z‖ < 1 := by
+    calc ‖conj w * z‖
+      _ = ‖w‖ * ‖z‖ := by simp
+      _ < 1 * 1 := by apply mul_lt_mul' <;> bound
+      _ = 1 := by norm_num
+  simp only [← e, one_mem, CStarRing.norm_of_mem_unitary, lt_self_iff_false] at lt
+
 /-- Convenience lemma to pull a inverse scale out of a Möbius denominator -/
 public lemma mobius_denom_inv_mul (r0 : r ≠ 0) (w z : ℂ) :
     (1 - conj (r⁻¹ * w) * (r⁻¹ * z)) = r⁻¹ ^ 2 * (r ^ 2 - conj w * z) := by