English
If f is differentiable on the ball ball c R1 and maps ball c R1 into ball (f c) R2, then the operator norm of the derivative at c satisfies ‖deriv f c‖ ≤ R2/R1.
Русский
Если f дифференцируема на шаре B(c, R1) и отображает этот шар в шар вокруг f(c) радиуса R2, то нормa производной в c не превосходит R2/R1.
LaTeX
$$$\|\mathrm{deriv} \, f \, c\| \le \dfrac{R_2}{R_1}$$$
Lean4
/-- 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 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
simpa only [dslope_same] using norm_dslope_le_div_of_mapsTo_ball hd h_maps (mem_ball_self h₀)
