English
If a family f_n: ℂ → E is locally uniformly summable on an open set s, and each f_n is differentiable at every point of s, then the sum z ↦ ∑' f_n(z) is differentiable on s.
Русский
Если семейство f_n: ℂ → E локально равномерно сходится по сумме на открытом множестве s и каждая f_n дифференцируема на s, то сумма ∑ f_n(z) дифференцируема на s.
LaTeX
$$$\text{IsOpen } s \to \text{SummableLocallyUniformlyOn } (f_n) s \to (\forall n, r, r \in s \to \text{DifferentiableAt } (f_n) r) \to \text{DifferentiableOn } (\lambda z, \sum' n, f_n z) s$$$
Lean4
theorem differentiableOn {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ι → ℂ → E}
{s : Set ℂ} (hs : IsOpen s) (h : SummableLocallyUniformlyOn (fun n ↦ ((fun z ↦ f n z))) s)
(hf2 : ∀ n r, r ∈ s → DifferentiableAt ℂ (f n) r) : DifferentiableOn ℂ (fun z ↦ ∑' n, f n z) s :=
by
obtain ⟨g, hg⟩ := h
have hc := (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).differentiableOn ?_ hs
· apply hc.congr
apply hg.tsum_eqOn
· filter_upwards with t r hr using DifferentiableWithinAt.fun_sum fun a ha ↦ (hf2 a r hr).differentiableWithinAt
