English
Exists delta>0 such that cthickening delta K ⊆ U and TendstoUniformlyOn of derivatives holds on K.
Русский
Существуют delta>0 такие, что cthickening(delta,K) ⊆ U и сходимость производных стабилизируется на K.
LaTeX
$$$\\exists δ>0, (\\text{cthickening } δ K) \\subseteq U ∧ TendstoUniformlyOn (deriv \\circ F) (cderiv δ f) φ K$$$
Lean4
theorem tendstoUniformlyOn_deriv_of_cthickening_subset (hf : TendstoLocallyUniformlyOn F f φ U)
(hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) {δ : ℝ} (hδ : 0 < δ) (hK : IsCompact K) (hU : IsOpen U)
(hKU : cthickening δ K ⊆ U) : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K :=
by
have h1 : ∀ᶠ n in φ, ContinuousOn (F n) (cthickening δ K) := by
filter_upwards [hF] with n h using h.continuousOn.mono hKU
have h2 : IsCompact (cthickening δ K) := hK.cthickening
have h3 : TendstoUniformlyOn F f φ (cthickening δ K) :=
(tendstoLocallyUniformlyOn_iff_forall_isCompact hU).mp hf (cthickening δ K) hKU h2
apply (h3.cderiv hδ h1).congr
filter_upwards [hF] with n h z hz
exact cderiv_eq_deriv hU h hδ ((closedBall_subset_cthickening hz δ).trans hKU)
