English
If a function f: ℂ→F is differentiable on a disc and the boundary values satisfy a uniform bound, then the norm of its derivative at the center is bounded by that bound divided by the radius.
Русский
Если функция f: ℂ→F дифференцируема на окружности и её значения на границе ограничены сверху константой, то норма производной в центре диска не превосходит этой константы, поделённой на радиус.
LaTeX
$$$\\|\\mathrm{deriv}\, f\\, c\\| \\le \\frac{C}{R} \\quad\\text{under } \\forall z\\in \\text{ball}(c,R),\\|f(z)\\|\\le C,$$$
Lean4
theorem norm_deriv_le_aux [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R)
(hf : DiffContOnCl ℂ f (ball c R)) (hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) : ‖deriv f c‖ ≤ C / R :=
by
have : ∀ z ∈ sphere c R, ‖(z - c) ^ (-2 : ℤ) • f z‖ ≤ C / (R * R) := fun z (hz : ‖z - c‖ = R) => by
simpa [-mul_inv_rev, norm_smul, hz, zpow_two, ← div_eq_inv_mul] using
(div_le_div_iff_of_pos_right (mul_pos hR hR)).2 (hC z hz)
calc
‖deriv f c‖ = ‖(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z‖ :=
congr_arg norm (deriv_eq_smul_circleIntegral hR hf)
_ ≤ R * (C / (R * R)) := (circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le this)
_ = C / R := by rw [mul_div_left_comm, div_self_mul_self', div_eq_mul_inv]
