/
Schwarz.lean
203 lines (168 loc) · 10.8 KB
/
Schwarz.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
/-
Copyright (c) 2022 Yury G. Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury G. Kudryashov
-/
import Mathlib.Analysis.Complex.AbsMax
import Mathlib.Analysis.Complex.RemovableSingularity
#align_import analysis.complex.schwarz from "leanprover-community/mathlib"@"3f655f5297b030a87d641ad4e825af8d9679eb0b"
/-!
# Schwarz lemma
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
center `f c` and radius `R₂`, then the absolute value 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
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 absolute value 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.abs_le_abs_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`.
## Implementation notes
We prove some versions of the Schwarz lemma for a map `f : ℂ → E` taking values in any normed space
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
-/
open Metric Set Function Filter TopologicalSpace
open scoped Topology
namespace Complex
section Space
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {R R₁ R₂ : ℝ} {f : ℂ → E}
{c z z₀ : ℂ}
/-- 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₁) :
‖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
refine' ge_of_tendsto _ this
exact (tendsto_const_nhds.div tendsto_id hR₁.ne').mono_left nhdsWithin_le_nhds
rw [mem_ball] at hz
filter_upwards [Ioo_mem_nhdsWithin_Iio ⟨hz, le_rfl⟩] with r hr
have hr₀ : 0 < r := dist_nonneg.trans_lt hr.1
replace hd : DiffContOnCl ℂ (dslope f c) (ball c r) := by
refine DifferentiableOn.diffContOnCl ?_
rw [closure_ball c hr₀.ne']
exact ((differentiableOn_dslope <| ball_mem_nhds _ hR₁).mpr hd).mono
(closedBall_subset_ball hr.2)
refine' norm_le_of_forall_mem_frontier_norm_le isBounded_ball hd _ _
· rw [frontier_ball c hr₀.ne']
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_right hr₀, ← dist_eq_norm]
exact le_of_lt (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
#align complex.schwarz_aux Complex.schwarz_aux
/-- 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₁) :
‖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⟩
rcases eq_or_ne (dslope f c z) 0 with hc | hc
· rw [hc, norm_zero]; exact div_nonneg hR₂.le 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₂
#align complex.norm_dslope_le_div_of_maps_to_ball Complex.norm_dslope_le_div_of_mapsTo_ball
/-- 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₂))
(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
have g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀ :=
isMaxOn_iff.mpr fun z hz => by simpa [h_eq] using g_le_div z hz
have g_diff : DifferentiableOn ℂ g (ball c R₁) :=
(differentiableOn_dslope (isOpen_ball.mem_nhds (mem_ball_self h_R₁))).mpr hd
have : g z = g z₀ := eqOn_of_isPreconnected_of_isMaxOn_norm (convex_ball c R₁).isPreconnected
isOpen_ball g_diff h_z₀ g_max hz
simp [g] at this
simp [g, ← this]
#align complex.affine_of_maps_to_ball_of_exists_norm_dslope_eq_div Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div
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_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₀
⟨dslope f c z₀, h_eq, affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div hd h_maps h_z₀ h_eq⟩
#align complex.affine_of_maps_to_ball_of_exists_norm_dslope_eq_div' Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div'
/-- The **Schwarz Lemma**: if `f : ℂ → E` sends an open disk with center `c` and a positive radius
`R₁` to an open ball with center `f c` and radius `R₂`, then the absolute value 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
simpa only [dslope_same] using norm_dslope_le_div_of_mapsTo_ball hd h_maps (mem_ball_self h₀)
#align complex.norm_deriv_le_div_of_maps_to_ball Complex.norm_deriv_le_div_of_mapsTo_ball
/-- 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
`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₁) :
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
#align complex.dist_le_div_mul_dist_of_maps_to_ball Complex.dist_le_div_mul_dist_of_mapsTo_ball
end Space
variable {f : ℂ → ℂ} {c z : ℂ} {R R₁ R₂ : ℝ}
/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk with center `c` and a positive radius
`R₁` to an open disk with center `f c` and radius `R₂`, then the absolute value of the derivative of
`f` at `c` is at most the ratio `R₂ / R₁`. -/
theorem abs_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₁) : abs (deriv f c) ≤ R₂ / R₁ :=
norm_deriv_le_div_of_mapsTo_ball hd h_maps h₀
#align complex.abs_deriv_le_div_of_maps_to_ball Complex.abs_deriv_le_div_of_mapsTo_ball
/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk of positive radius to itself and the
center of this disk to itself, then the absolute value of the derivative of `f` at the center of
this disk is at most `1`. -/
theorem abs_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) : abs (deriv f c) ≤ 1 :=
(norm_deriv_le_div_of_mapsTo_ball hd (by rwa [hc]) h₀).trans_eq (div_self h₀.ne')
#align complex.abs_deriv_le_one_of_maps_to_ball Complex.abs_deriv_le_one_of_mapsTo_ball
/-- 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
-- Porting note: `simp` was failing to use `div_self`
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'
#align complex.dist_le_dist_of_maps_to_ball_self Complex.dist_le_dist_of_mapsTo_ball_self
/-- The **Schwarz Lemma**: 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`. -/
theorem abs_le_abs_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 : abs z < R) :
abs (f z) ≤ abs 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
#align complex.abs_le_abs_of_maps_to_ball_self Complex.abs_le_abs_of_mapsTo_ball_self
end Complex