feat: weaken assumptions in Schwarz lemma (leanprover-community#33362)

Assume that `f` maps an open ball to a closed ball.
Also, generalize the "same radius" versions to any codomain.

Author: urkud

Mathlib/Analysis/Complex/Schwarz.lean

@@ -14,21 +14,21 @@ public import Mathlib.Analysis.Complex.RemovableSingularity
 In this file we prove several versions of the Schwarz lemma.
 
 * `Complex.norm_deriv_le_div_of_mapsTo_ball`, `Complex.abs_deriv_le_div_of_mapsTo_ball`: if
-  `f : ℂ → E` sends an open disk with center `c` and a positive radius `R₁` to an open ball with
+  `f : ℂ → E` sends an open disk with center `c` and a positive radius `R₁` to a closed ball with
   center `f c` and radius `R₂`, then the norm of the derivative of `f` at `c` is at most
   the ratio `R₂ / R₁`;
 
 * `Complex.dist_le_div_mul_dist_of_mapsTo_ball`: if `f : ℂ → E` sends an open disk with center `c`
-  and radius `R₁` to an open disk with center `f c` and radius `R₂`, then for any `z` in the former
+  and radius `R₁` to a closed disk with center `f c` and radius `R₂`, then for any `z` in the former
   disk we have `dist (f z) (f c) ≤ (R₂ / R₁) * dist z c`;
 
-* `Complex.abs_deriv_le_one_of_mapsTo_ball`: if `f : ℂ → ℂ` sends an open disk of positive radius
-  to itself and the center of this disk to itself, then the norm of the derivative of `f`
-  at the center of this disk is at most `1`;
+* `Complex.abs_deriv_le_one_of_mapsTo_ball`: if `f : ℂ → ℂ` sends a point `c` to itself
+  and it maps an open disk with center `c` to the closed disk with the same center and radius,
+  then the norm of the derivative of `f` at the center of this disk is at most `1`;
 
-* `Complex.dist_le_dist_of_mapsTo_ball_self`: if `f : ℂ → ℂ` sends an open disk to itself and the
-  center `c` of this disk to itself, then for any point `z` of this disk we have
-  `dist (f z) c ≤ dist z c`;
+* `Complex.dist_le_dist_of_mapsTo_ball_self`: if `f : ℂ → ℂ` sends a point `c` to itself
+  and it maps an open disk with center `c` to the closed disk with the same center and radius,
+  then for any point `z` of this disk we have `dist (f z) c ≤ dist z c`;
 
 * `Complex.norm_le_norm_of_mapsTo_ball_self`: if `f : ℂ → ℂ` sends an open disk with center `0` to
   itself, then for any point `z` of this disk we have `abs (f z) ≤ abs z`.
@@ -40,32 +40,25 @@ over complex numbers.
 
 ## TODO
 
-* Prove that these inequalities are strict unless `f` is an affine map.
-
 * Prove that any diffeomorphism of the unit disk to itself is a Möbius map.
 
 ## Tags
 
 Schwarz lemma
 -/
 
-@[expose] public section
-
-
 open Metric Set Function Filter TopologicalSpace
 
-open scoped Topology
+open scoped Topology ComplexConjugate
 
-namespace Complex
-
-section Space
-
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E}
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {R R₁ R₂ : ℝ} {f : ℂ → E}
   {c z z₀ : ℂ}
 
+namespace Complex
+
 /-- An auxiliary lemma for `Complex.norm_dslope_le_div_of_mapsTo_ball`. -/
 theorem schwarz_aux {f : ℂ → ℂ} (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
+    (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)) (hz : z ∈ ball c R₁) :
     ‖dslope f c z‖ ≤ R₂ / R₁ := by
   have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
   suffices ∀ᶠ r in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r by
@@ -84,39 +77,40 @@ theorem schwarz_aux {f : ℂ → ℂ} (hd : DifferentiableOn ℂ f (ball c R₁)
     intro z hz
     have hz' : z ≠ c := ne_of_mem_sphere hz hr₀.ne'
     rw [dslope_of_ne _ hz', slope_def_module, norm_smul, norm_inv, mem_sphere_iff_norm.1 hz, ←
-      div_eq_inv_mul, div_le_div_iff_of_pos_right hr₀, ← dist_eq_norm]
-    exact le_of_lt (h_maps (mem_ball.2 (by rw [mem_sphere.1 hz]; exact hr.2)))
+      div_eq_inv_mul, div_le_div_iff_of_pos_right hr₀, ← mem_closedBall_iff_norm]
+    exact h_maps <| mem_ball.2 <| by rw [mem_sphere.1 hz]; exact hr.2
   · rw [closure_ball c hr₀.ne', mem_closedBall]
     exact hr.1.le
 
+public section
+
 /-- Two cases of the **Schwarz Lemma** (derivative and distance), merged together. -/
 theorem norm_dslope_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
+    (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)) (hz : z ∈ ball c R₁) :
     ‖dslope f c z‖ ≤ R₂ / R₁ := by
   have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
-  have hR₂ : 0 < R₂ := nonempty_ball.1 ⟨f z, h_maps hz⟩
+  have hR₂ : 0 ≤ R₂ := nonempty_closedBall.mp ⟨f z, h_maps hz⟩
   rcases eq_or_ne (dslope f c z) 0 with hc | hc
-  · rw [hc, norm_zero]; exact div_nonneg hR₂.le hR₁.le
+  · rw [hc, norm_zero]; exact div_nonneg hR₂ hR₁.le
   rcases exists_dual_vector ℂ _ hc with ⟨g, hg, hgf⟩
   have hg' : ‖g‖₊ = 1 := NNReal.eq hg
-  have hg₀ : ‖g‖₊ ≠ 0 := by simpa only [hg'] using one_ne_zero
   calc
     ‖dslope f c z‖ = ‖dslope (g ∘ f) c z‖ := by
       rw [g.dslope_comp, hgf, RCLike.norm_ofReal, abs_norm]
       exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)
     _ ≤ R₂ / R₁ := by
       refine schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp ?_ h_maps) hz
-      simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂
+      simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_closedBall (f c) R₂
 
 /-- Equality case in the **Schwarz Lemma**: in the setup of `norm_dslope_le_div_of_mapsTo_ball`, if
 `‖dslope f c z₀‖ = R₂ / R₁` holds at a point in the ball then the map `f` is affine. -/
 theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div [CompleteSpace E] [StrictConvexSpace ℝ E]
-    (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : Set.MapsTo f (ball c R₁) (ball (f c) R₂))
+    (hd : DifferentiableOn ℂ f (ball c R₁))
+    (h_maps : Set.MapsTo f (ball c R₁) (closedBall (f c) R₂))
     (h_z₀ : z₀ ∈ ball c R₁) (h_eq : ‖dslope f c z₀‖ = R₂ / R₁) :
     Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (ball c R₁) := by
   set g := dslope f c
   rintro z hz
-  by_cases h : z = c; · simp [h]
   have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩
   have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz =>
     norm_dslope_le_div_of_mapsTo_ball hd h_maps hz
@@ -131,7 +125,7 @@ theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div [CompleteSpace E] [St
 
 theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div' [CompleteSpace E]
     [StrictConvexSpace ℝ E] (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : Set.MapsTo f (ball c R₁) (ball (f c) R₂))
+    (h_maps : Set.MapsTo f (ball c R₁) (closedBall (f c) R₂))
     (h_z₀ : ∃ z₀ ∈ ball c R₁, ‖dslope f c z₀‖ = R₂ / R₁) :
     ∃ C : E, ‖C‖ = R₂ / R₁ ∧ Set.EqOn f (fun z => f c + (z - c) • C) (ball c R₁) :=
   let ⟨z₀, h_z₀, h_eq⟩ := h_z₀
@@ -141,46 +135,43 @@ theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div' [CompleteSpace E]
 `R₁` to an open ball with center `f c` and radius `R₂`, then the norm of the derivative of
 `f` at `c` is at most the ratio `R₂ / R₁`. -/
 theorem norm_deriv_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (h₀ : 0 < R₁) : ‖deriv f c‖ ≤ R₂ / R₁ := by
+    (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)) (h₀ : 0 < R₁) :
+    ‖deriv f c‖ ≤ R₂ / R₁ := by
   simpa only [dslope_same] using norm_dslope_le_div_of_mapsTo_ball hd h_maps (mem_ball_self h₀)
 
-/-- The **Schwarz Lemma**: if `f : ℂ → E` sends an open disk with center `c` and radius `R₁` to an
-open ball with center `f c` and radius `R₂`, then for any `z` in the former disk we have
+/-- The **Schwarz Lemma**: if `f : ℂ → E` sends an open disk with center `c` and radius `R₁` to a
+closed ball with center `f c` and radius `R₂`, then for any `z` in the former disk we have
 `dist (f z) (f c) ≤ (R₂ / R₁) * dist z c`. -/
 theorem dist_le_div_mul_dist_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
-    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
+    (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)) (hz : z ∈ ball c R₁) :
     dist (f z) (f c) ≤ R₂ / R₁ * dist z c := by
   rcases eq_or_ne z c with (rfl | hne)
   · simp only [dist_self, mul_zero, le_rfl]
   simpa only [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← div_eq_inv_mul, ←
     dist_eq_norm, div_le_iff₀ (dist_pos.2 hne)] using norm_dslope_le_div_of_mapsTo_ball hd h_maps hz
 
-end Space
-
-variable {f : ℂ → ℂ} {c z : ℂ} {R R₁ R₂ : ℝ}
-
 /-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk of positive radius to itself and the
 center of this disk to itself, then the norm of the derivative of `f` at the center of
 this disk is at most `1`. -/
 theorem norm_deriv_le_one_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R))
-    (h_maps : MapsTo f (ball c R) (ball c R)) (hc : f c = c) (h₀ : 0 < R) : ‖deriv f c‖ ≤ 1 :=
-  (norm_deriv_le_div_of_mapsTo_ball hd (by rwa [hc]) h₀).trans_eq (div_self h₀.ne')
+    (h_maps : MapsTo f (ball c R) (closedBall (f c) R)) (h₀ : 0 < R) : ‖deriv f c‖ ≤ 1 :=
+  (norm_deriv_le_div_of_mapsTo_ball hd h_maps h₀).trans_eq (div_self h₀.ne')
 
 /-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk to itself and the center `c` of this
 disk to itself, then for any point `z` of this disk we have `dist (f z) c ≤ dist z c`. -/
 theorem dist_le_dist_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball c R))
-    (h_maps : MapsTo f (ball c R) (ball c R)) (hc : f c = c) (hz : z ∈ ball c R) :
-    dist (f z) c ≤ dist z c := by
-  have := dist_le_div_mul_dist_of_mapsTo_ball hd (by rwa [hc]) hz
-  rwa [hc, div_self, one_mul] at this
-  exact (nonempty_ball.1 ⟨z, hz⟩).ne'
-
-/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk with center `0` to itself, then for any
-point `z` of this disk we have `‖f z‖ ≤ ‖z‖`. -/
+    (h_maps : MapsTo f (ball c R) (closedBall (f c) R)) (hz : z ∈ ball c R) :
+    dist (f z) (f c) ≤ dist z c := by
+  simpa [(nonempty_ball.1 ⟨z, hz⟩).ne'] using dist_le_div_mul_dist_of_mapsTo_ball hd h_maps hz
+
+/-- The **Schwarz Lemma**: if `f : ℂ → E` sends an open disk with center `0`
+to the closed ball with center `0` of the same radius,
+then for any point `z` of this disk we have `‖f z‖ ≤ ‖z‖`. -/
 theorem norm_le_norm_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball 0 R))
-    (h_maps : MapsTo f (ball 0 R) (ball 0 R)) (h₀ : f 0 = 0) (hz : ‖z‖ < R) :
+    (h_maps : MapsTo f (ball 0 R) (closedBall 0 R)) (h₀ : f 0 = 0) (hz : ‖z‖ < R) :
     ‖f z‖ ≤ ‖z‖ := by
-  replace hz : z ∈ ball (0 : ℂ) R := mem_ball_zero_iff.2 hz
-  simpa only [dist_zero_right] using dist_le_dist_of_mapsTo_ball_self hd h_maps h₀ hz
+  simpa [h₀] using dist_le_dist_of_mapsTo_ball_self hd (by rwa [h₀]) (mem_ball_zero_iff.mpr hz)
+
+end -- public section
 
 end Complex