English
If f maps ball c R1 into ball (f(c)) R2 and is differentiable on that ball, then for every z in ball c R1 we have dist(f(z), f(c)) ≤ (R2/R1) · dist(z, c).
Русский
Если f отображает шар B(c,R1) в шар вокруг f(c) радиуса R2 и дифференцируема на этом шаре, то для каждого z∈B(c,R1): dist(f(z), f(c)) ≤ (R2/R1)·dist(z, c).
LaTeX
$$$\mathrm{dist}(f(z), f(c)) \le \dfrac{R_2}{R_1} \cdot \mathrm{dist}(z,c)\quad (z \in \mathrm{ball}\ c\ R_1)$$$
Lean4
/-- 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
