English
In the Schwarz lemma context, if the derivative bound is attained, the map is necessarily affine on the ball.
Русский
В контексте леммы Шварца, при достижении предельной границы производной, отображение должно быть аффином на шаре.
LaTeX
$$$\text{Если } \|dslope f c z0\| = R_2/R_1, \ f \text{affine on } \mathrm{Ball}(c,R_1).$$$
Lean4
/-- 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_nhdsLT hz] 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_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)))
· rw [closure_ball c hr₀.ne', mem_closedBall]
exact hr.1.le
