English
If on a circle the values of f are bounded and a Liouville-type bound holds, then ‖cderiv r f z‖ ≤ M/r.
Русский
Если на окружности значения f ограничены и выполняется ограничение Лиуильля, то ‖cderiv r f z‖ ≤ M/r.
LaTeX
$$$\\|\\mathrm{cderiv}\\, r\\, f\\, z\\| ≤ \\frac{M}{r}$ under appropriate hypotheses$$
Lean4
theorem _root_.TendstoLocallyUniformlyOn.deriv (hf : TendstoLocallyUniformlyOn F f φ U)
(hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) :
TendstoLocallyUniformlyOn (deriv ∘ F) (deriv f) φ U :=
by
rw [tendstoLocallyUniformlyOn_iff_forall_isCompact hU]
rcases φ.eq_or_neBot with rfl | hne
· simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
rintro K hKU hK
obtain ⟨δ, hδ, hK4, h⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
refine h.congr_right fun z hz => cderiv_eq_deriv hU (hf.differentiableOn hF hU) hδ ?_
exact (closedBall_subset_cthickening hz δ).trans hK4
