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 (fun (n : ι) (z : ℂ) => f n z) s) (hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r) : DifferentiableOn ℂ (fun (z : ℂ) => ∑' (n : ι), f n z) s