Differentiability of uniformly convergent series sums of functions #
We collect some results about the differentiability of infinite sums.
theorem
SummableLocallyUniformlyOn.differentiableOn
{ι : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[CompleteSpace E]
{f : ι → ℂ → E}
{s : Set ℂ}
(hs : IsOpen s)
(h : SummableLocallyUniformlyOn f s)
(hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r)
:
DifferentiableOn ℂ (fun (z : ℂ) => ∑' (n : ι), f n z) s