norm_deriv_le_one_of_mapsTo_ball — Mathlib

English

If f maps a ball into itself and fixes the center c (f(c) = c), then ‖deriv f c‖ ≤ 1.

Русский

Если f отображает шар в него самого и фиксирует центр (f(c) = c), то ‖f'(c)‖ ≤ 1.

LaTeX

$$$\|\mathrm{deriv} f c\| \le 1$$$

Lean4

/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk of positive radius to itself and the
center of this disk to itself, then the norm of the derivative of `f` at the center of
this disk is at most `1`. -/
theorem norm_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) : ‖deriv f c‖ ≤ 1 :=
  (norm_deriv_le_div_of_mapsTo_ball hd (by rwa [hc]) h₀).trans_eq (div_self h₀.ne')

Похожие утверждения