English
If a function is differentiable on a circle and the boundary values are bounded by M, then the norm of cderiv is bounded by M/r.
Русский
Если функция дифференцируема на окружности и значения на границе ограничены M, то ||cderiv|| ≤ M/r.
LaTeX
$$$\\| \\mathrm{cderiv}\\; r \\; f \\; z \\| \\le \\frac{M}{r} \\quad\\text{whenever } z\\in \\mathbb{C}, r>0, \\|f(w)\\| ≤ M \\text{ on } w\\in \\mathrm{sphere}(z,r)$$$
Lean4
theorem cderiv_sub (hr : 0 < r) (hf : ContinuousOn f (sphere z r)) (hg : ContinuousOn g (sphere z r)) :
cderiv r (f - g) z = cderiv r f z - cderiv r g z :=
by
have h1 : ContinuousOn (fun w : ℂ => ((w - z) ^ 2)⁻¹) (sphere z r) :=
by
refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne ?_
rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw
simp_rw [cderiv, ← smul_sub]
congr 1
simpa only [Pi.sub_apply, smul_sub] using
circleIntegral.integral_sub ((h1.smul hf).circleIntegrable hr.le) ((h1.smul hg).circleIntegrable hr.le)
