English
There exists δ>0 such that the derivative sequence tends to the cderiv of f uniformly on K within U.
Русский
Существует δ>0 такое, что сходится по униформности производная последовательности к cderiv f на K внутри U.
LaTeX
$$$\\exists δ>0, (\\operatorname{cthickening} δ K) \\subseteq U \\wedge TendstoUniformlyOn (deriv \\circ F) (cderiv δ f) φ K$$$
Lean4
theorem norm_cderiv_le (hr : 0 < r) (hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M) : ‖cderiv r f z‖ ≤ M / r :=
by
have hM : 0 ≤ M := by
obtain ⟨w, hw⟩ : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
exact (norm_nonneg _).trans (hf w hw)
have h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2 :=
by
intro w hw
simp only [mem_sphere_iff_norm] at hw
simp only [norm_smul, inv_mul_eq_div, hw, norm_inv, norm_pow]
exact div_le_div₀ hM (hf w hw) (sq_pos_of_pos hr) le_rfl
have h2 := circleIntegral.norm_integral_le_of_norm_le_const hr.le h1
simp only [cderiv, norm_smul]
refine (mul_le_mul le_rfl h2 (norm_nonneg _) (norm_nonneg _)).trans (le_of_eq ?_)
simp [field, abs_of_nonneg Real.pi_pos.le]
