Skip to content

Commit 0c2078a

Browse files
urkudurkud
committed
feat: port Analysis.Complex.Schwarz (#4910)
1 parent 45c9d61 commit 0c2078a

File tree

2 files changed

+204
-0
lines changed

2 files changed

+204
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -520,6 +520,7 @@ import Mathlib.Analysis.Complex.OperatorNorm
520520
import Mathlib.Analysis.Complex.ReImTopology
521521
import Mathlib.Analysis.Complex.RealDeriv
522522
import Mathlib.Analysis.Complex.RemovableSingularity
523+
import Mathlib.Analysis.Complex.Schwarz
523524
import Mathlib.Analysis.Complex.UnitDisc.Basic
524525
import Mathlib.Analysis.Convex.Basic
525526
import Mathlib.Analysis.Convex.Between

‎Mathlib/Analysis/Complex/Schwarz.lean‎

Lines changed: 203 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,203 @@
1+
/-
2+
Copyright (c) 2022 Yury G. Kudryashov. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yury G. Kudryashov
5+
6+
! This file was ported from Lean 3 source module analysis.complex.schwarz
7+
! leanprover-community/mathlib commit 3f655f5297b030a87d641ad4e825af8d9679eb0b
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Analysis.Complex.AbsMax
12+
import Mathlib.Analysis.Complex.RemovableSingularity
13+
14+
/-!
15+
# Schwarz lemma
16+
17+
In this file we prove several versions of the Schwarz lemma.
18+
19+
* `Complex.norm_deriv_le_div_of_mapsTo_ball`, `Complex.abs_deriv_le_div_of_mapsTo_ball`: if
20+
`f : ℂ → E` sends an open disk with center `c` and a positive radius `R₁` to an open ball with
21+
center `f c` and radius `R₂`, then the absolute value of the derivative of `f` at `c` is at most
22+
the ratio `R₂ / R₁`;
23+
24+
* `Complex.dist_le_div_mul_dist_of_mapsTo_ball`: if `f : ℂ → E` sends an open disk with center `c`
25+
and radius `R₁` to an open disk with center `f c` and radius `R₂`, then for any `z` in the former
26+
disk we have `dist (f z) (f c) ≤ (R₂ / R₁) * dist z c`;
27+
28+
* `Complex.abs_deriv_le_one_of_mapsTo_ball`: if `f : ℂ → ℂ` sends an open disk of positive radius
29+
to itself and the center of this disk to itself, then the absolute value of the derivative of `f`
30+
at the center of this disk is at most `1`;
31+
32+
* `complex.dist_le_dist_of_maps_to_ball`: if `f : ℂ → ℂ` sends an open disk to itself and the center
33+
`c` of this disk to itself, then for any point `z` of this disk we have `dist (f z) c ≤ dist z c`;
34+
35+
* `complex.abs_le_abs_of_maps_to_ball`: if `f : ℂ → ℂ` sends an open disk with center `0` to itself,
36+
then for any point `z` of this disk we have `abs (f z) ≤ abs z`.
37+
38+
## Implementation notes
39+
40+
We prove some versions of the Schwarz lemma for a map `f : ℂ → E` taking values in any normed space
41+
over complex numbers.
42+
43+
## TODO
44+
45+
* Prove that these inequalities are strict unless `f` is an affine map.
46+
47+
* Prove that any diffeomorphism of the unit disk to itself is a Möbius map.
48+
49+
## Tags
50+
51+
Schwarz lemma
52+
-/
53+
54+
55+
open Metric Set Function Filter TopologicalSpace
56+
57+
open scoped Topology
58+
59+
namespace Complex
60+
61+
section Space
62+
63+
variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℂ E] {R R₁ R₂ : ℝ} {f : ℂ → E}
64+
{c z z₀ : ℂ}
65+
66+
/-- An auxiliary lemma for `Complex.norm_dslope_le_div_of_mapsTo_ball`. -/
67+
theorem schwarz_aux {f : ℂ → ℂ} (hd : DifferentiableOn ℂ f (ball c R₁))
68+
(h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
69+
‖dslope f c z‖ ≤ R₂ / R₁ := by
70+
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
71+
suffices ∀ᶠ r in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r by
72+
refine' ge_of_tendsto _ this
73+
exact (tendsto_const_nhds.div tendsto_id hR₁.ne').mono_left nhdsWithin_le_nhds
74+
rw [mem_ball] at hz
75+
filter_upwards [Ioo_mem_nhdsWithin_Iio ⟨hz, le_rfl⟩] with r hr
76+
have hr₀ : 0 < r := dist_nonneg.trans_lt hr.1
77+
replace hd : DiffContOnCl ℂ (dslope f c) (ball c r)
78+
· refine' DifferentiableOn.diffContOnCl _
79+
rw [closure_ball c hr₀.ne']
80+
exact ((differentiableOn_dslope <| ball_mem_nhds _ hR₁).mpr hd).mono
81+
(closedBall_subset_ball hr.2)
82+
refine' norm_le_of_forall_mem_frontier_norm_le bounded_ball hd _ _
83+
· rw [frontier_ball c hr₀.ne']
84+
intro z hz
85+
have hz' : z ≠ c := ne_of_mem_sphere hz hr₀.ne'
86+
rw [dslope_of_ne _ hz', slope_def_module, norm_smul, norm_inv, mem_sphere_iff_norm.1 hz, ←
87+
div_eq_inv_mul, div_le_div_right hr₀, ← dist_eq_norm]
88+
exact le_of_lt (h_maps (mem_ball.2 (by rw [mem_sphere.1 hz]; exact hr.2)))
89+
· rw [closure_ball c hr₀.ne', mem_closedBall]
90+
exact hr.1.le
91+
#align complex.schwarz_aux Complex.schwarz_aux
92+
93+
/-- Two cases of the **Schwarz Lemma** (derivative and distance), merged together. -/
94+
theorem norm_dslope_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
95+
(h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
96+
‖dslope f c z‖ ≤ R₂ / R₁ := by
97+
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
98+
have hR₂ : 0 < R₂ := nonempty_ball.1 ⟨f z, h_maps hz⟩
99+
cases' eq_or_ne (dslope f c z) 0 with hc hc
100+
· rw [hc, norm_zero]; exact div_nonneg hR₂.le hR₁.le
101+
rcases exists_dual_vector ℂ _ hc with ⟨g, hg, hgf⟩
102+
have hg' : ‖g‖₊ = 1 := NNReal.eq hg
103+
have hg₀ : ‖g‖₊ ≠ 0 := by simpa only [hg'] using one_ne_zero
104+
calc
105+
‖dslope f c z‖ = ‖dslope (g ∘ f) c z‖ := by
106+
rw [g.dslope_comp, hgf, IsROrC.norm_ofReal, abs_norm]
107+
exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)
108+
_ ≤ R₂ / R₁ := by
109+
refine' schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp _ h_maps) hz
110+
simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂
111+
#align complex.norm_dslope_le_div_of_maps_to_ball Complex.norm_dslope_le_div_of_mapsTo_ball
112+
113+
/-- Equality case in the **Schwarz Lemma**: in the setup of `norm_dslope_le_div_of_maps_to_ball`, if
114+
`‖dslope f c z₀‖ = R₂ / R₁` holds at a point in the ball then the map `f` is affine. -/
115+
theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div [CompleteSpace E] [StrictConvexSpace ℝ E]
116+
(hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : Set.MapsTo f (ball c R₁) (ball (f c) R₂))
117+
(h_z₀ : z₀ ∈ ball c R₁) (h_eq : ‖dslope f c z₀‖ = R₂ / R₁) :
118+
Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (ball c R₁) := by
119+
set g := dslope f c
120+
rintro z hz
121+
by_cases z = c; · simp [h]
122+
have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩
123+
have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz =>
124+
norm_dslope_le_div_of_mapsTo_ball hd h_maps hz
125+
have g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀ :=
126+
isMaxOn_iff.mpr fun z hz => by simpa [h_eq] using g_le_div z hz
127+
have g_diff : DifferentiableOn ℂ g (ball c R₁) :=
128+
(differentiableOn_dslope (isOpen_ball.mem_nhds (mem_ball_self h_R₁))).mpr hd
129+
have : g z = g z₀ := eqOn_of_isPreconnected_of_isMaxOn_norm (convex_ball c R₁).isPreconnected
130+
isOpen_ball g_diff h_z₀ g_max hz
131+
simp [← this]
132+
#align complex.affine_of_maps_to_ball_of_exists_norm_dslope_eq_div Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div
133+
134+
theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div' [CompleteSpace E]
135+
[StrictConvexSpace ℝ E] (hd : DifferentiableOn ℂ f (ball c R₁))
136+
(h_maps : Set.MapsTo f (ball c R₁) (ball (f c) R₂))
137+
(h_z₀ : ∃ z₀ ∈ ball c R₁, ‖dslope f c z₀‖ = R₂ / R₁) :
138+
∃ C : E, ‖C‖ = R₂ / R₁ ∧ Set.EqOn f (fun z => f c + (z - c) • C) (ball c R₁) :=
139+
let ⟨z₀, h_z₀, h_eq⟩ := h_z₀
140+
⟨dslope f c z₀, h_eq, affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div hd h_maps h_z₀ h_eq⟩
141+
#align complex.affine_of_maps_to_ball_of_exists_norm_dslope_eq_div' Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div'
142+
143+
/-- The **Schwarz Lemma**: if `f : ℂ → E` sends an open disk with center `c` and a positive radius
144+
`R₁` to an open ball with center `f c` and radius `R₂`, then the absolute value of the derivative of
145+
`f` at `c` is at most the ratio `R₂ / R₁`. -/
146+
theorem norm_deriv_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
147+
(h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (h₀ : 0 < R₁) : ‖deriv f c‖ ≤ R₂ / R₁ := by
148+
simpa only [dslope_same] using norm_dslope_le_div_of_mapsTo_ball hd h_maps (mem_ball_self h₀)
149+
#align complex.norm_deriv_le_div_of_maps_to_ball Complex.norm_deriv_le_div_of_mapsTo_ball
150+
151+
/-- The **Schwarz Lemma**: if `f : ℂ → E` sends an open disk with center `c` and radius `R₁` to an
152+
open ball with center `f c` and radius `R₂`, then for any `z` in the former disk we have
153+
`dist (f z) (f c) ≤ (R₂ / R₁) * dist z c`. -/
154+
theorem dist_le_div_mul_dist_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
155+
(h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
156+
dist (f z) (f c) ≤ R₂ / R₁ * dist z c := by
157+
rcases eq_or_ne z c with (rfl | hne);
158+
· simp only [dist_self, mul_zero, le_rfl]
159+
simpa only [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← div_eq_inv_mul, ←
160+
dist_eq_norm, div_le_iff (dist_pos.2 hne)] using norm_dslope_le_div_of_mapsTo_ball hd h_maps hz
161+
#align complex.dist_le_div_mul_dist_of_maps_to_ball Complex.dist_le_div_mul_dist_of_mapsTo_ball
162+
163+
end Space
164+
165+
variable {f : ℂ → ℂ} {c z : ℂ} {R R₁ R₂ : ℝ}
166+
167+
/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk with center `c` and a positive radius
168+
`R₁` to an open disk with center `f c` and radius `R₂`, then the absolute value of the derivative of
169+
`f` at `c` is at most the ratio `R₂ / R₁`. -/
170+
theorem abs_deriv_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
171+
(h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (h₀ : 0 < R₁) : abs (deriv f c) ≤ R₂ / R₁ :=
172+
norm_deriv_le_div_of_mapsTo_ball hd h_maps h₀
173+
#align complex.abs_deriv_le_div_of_maps_to_ball Complex.abs_deriv_le_div_of_mapsTo_ball
174+
175+
/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk of positive radius to itself and the
176+
center of this disk to itself, then the absolute value of the derivative of `f` at the center of
177+
this disk is at most `1`. -/
178+
theorem abs_deriv_le_one_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R))
179+
(h_maps : MapsTo f (ball c R) (ball c R)) (hc : f c = c) (h₀ : 0 < R) : abs (deriv f c) ≤ 1 :=
180+
(norm_deriv_le_div_of_mapsTo_ball hd (by rwa [hc]) h₀).trans_eq (div_self h₀.ne')
181+
#align complex.abs_deriv_le_one_of_maps_to_ball Complex.abs_deriv_le_one_of_mapsTo_ball
182+
183+
/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk to itself and the center `c` of this
184+
disk to itself, then for any point `z` of this disk we have `dist (f z) c ≤ dist z c`. -/
185+
theorem dist_le_dist_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball c R))
186+
(h_maps : MapsTo f (ball c R) (ball c R)) (hc : f c = c) (hz : z ∈ ball c R) :
187+
dist (f z) c ≤ dist z c := by
188+
-- porting note: `simp` was failing to use `div_self`
189+
have := dist_le_div_mul_dist_of_mapsTo_ball hd (by rwa [hc]) hz
190+
rwa [hc, div_self, one_mul] at this
191+
exact (nonempty_ball.1 ⟨z, hz⟩).ne'
192+
#align complex.dist_le_dist_of_maps_to_ball_self Complex.dist_le_dist_of_mapsTo_ball_self
193+
194+
/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk with center `0` to itself, the for any
195+
point `z` of this disk we have `abs (f z) ≤ abs z`. -/
196+
theorem abs_le_abs_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball 0 R))
197+
(h_maps : MapsTo f (ball 0 R) (ball 0 R)) (h₀ : f 0 = 0) (hz : abs z < R) :
198+
abs (f z) ≤ abs z := by
199+
replace hz : z ∈ ball (0 : ℂ) R; exact mem_ball_zero_iff.2 hz
200+
simpa only [dist_zero_right] using dist_le_dist_of_mapsTo_ball_self hd h_maps h₀ hz
201+
#align complex.abs_le_abs_of_maps_to_ball_self Complex.abs_le_abs_of_mapsTo_ball_self
202+
203+
end Complex

0 commit comments

Comments
 (0)