English
The tsum of differentiable maps, bounded by a summable majorant, is differentiable on an open set.
Русский
Сумма по индексам бесконечной суммы дифференцируемых отображений, ограниченная суммируемым мажорантом, дифференцируема на открытом множестве.
LaTeX
$$$DifferentiableOn\\ (\\lambda w, \\operatorname{tsum}_{i} F_i w)\\ U$$$
Lean4
/-- A locally uniform limit of holomorphic functions on an open domain of the complex plane is
holomorphic (the derivatives converge locally uniformly to that of the limit, which is proved
as `TendstoLocallyUniformlyOn.deriv`). -/
theorem _root_.TendstoLocallyUniformlyOn.differentiableOn [φ.NeBot] (hf : TendstoLocallyUniformlyOn F f φ U)
(hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) : DifferentiableOn ℂ f U :=
by
rintro x hx
obtain ⟨K, ⟨hKx, hK⟩, hKU⟩ := (compact_basis_nhds x).mem_iff.mp (hU.mem_nhds hx)
obtain ⟨δ, _, _, h1⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
have h2 : interior K ⊆ U := interior_subset.trans hKU
have h3 : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) (interior K) := by filter_upwards [hF] with n h using h.mono h2
have h4 : TendstoLocallyUniformlyOn F f φ (interior K) := hf.mono h2
have h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K) :=
h1.tendstoLocallyUniformlyOn.mono interior_subset
have h6 : ∀ x ∈ interior K, HasDerivAt f (cderiv δ f x) x := fun x h =>
hasDerivAt_of_tendsto_locally_uniformly_on' isOpen_interior h5 h3 (fun _ => h4.tendsto_at) h
have h7 : DifferentiableOn ℂ f (interior K) := fun x hx => (h6 x hx).differentiableAt.differentiableWithinAt
exact (h7.differentiableAt (interior_mem_nhds.mpr hKx)).differentiableWithinAt
