exists_cthickening_tendstoUniformlyOn

English

Under locally uniform convergence on a ct thickening, derivative convergence holds uniformly on K.

Русский

При локальной равномерной сходимости на ct-уплотнении производная сходится равномерно на K.

LaTeX

$$$TendstoUniformlyOn (Function.comp deriv F) (Complex.cderiv δ f) φ K$ under the stated hypotheses$$

Lean4

theorem exists_cthickening_tendstoUniformlyOn (hf : TendstoLocallyUniformlyOn F f φ U)
    (hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
    ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K :=
  by
  obtain ⟨δ, hδ, hKδ⟩ := hK.exists_cthickening_subset_open hU hKU
  exact ⟨δ, hδ, hKδ, tendstoUniformlyOn_deriv_of_cthickening_subset hf hF hδ hK hU hKδ⟩

Похожие утверждения