Differentiability of sum of functions

We prove some HasSumUniformlyOn versions of theorems from Mathlib.Analysis.NormedSpace.FunctionSeries.

Alongside this we prove derivWithin_tsum which states that the derivative of a series of functions is the sum of the derivatives, under suitable conditions we also prove an iteratedDerivWithin version.

theorem HasSumUniformlyOn.of_norm_le_summable {α : Type u_1} {β : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} {f : α → β → F} (hu : Summable u) {s : Set β} (hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n) : HasSumUniformlyOn f (fun (x : β) => ∑' (n : α), f n x) {s}

theorem HasSumUniformlyOn.of_norm_le_summable_eventually {β : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [CompleteSpace F] {ι : Type u_4} {f : ι → β → F} {u : ι → ℝ} (hu : Summable u) {s : Set β} (hfu : ∀ᶠ (n : ι) in Filter.cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n) : HasSumUniformlyOn f (fun (x : β) => ∑' (n : ι), f n x) {s}

theorem SummableLocallyUniformlyOn.of_locally_bounded_eventually {α : Type u_1} {β : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [CompleteSpace F] [TopologicalSpace β] [LocallyCompactSpace β] {f : α → β → F} {s : Set β} (hs : IsOpen s) (hu : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in Filter.cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n) : SummableLocallyUniformlyOn f s

theorem SummableLocallyUniformlyOn_of_locally_bounded {α : Type u_1} {β : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [CompleteSpace F] [TopologicalSpace β] [LocallyCompactSpace β] {f : α → β → F} {s : Set β} (hs : IsOpen s) (hu : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n) : SummableLocallyUniformlyOn f s

theorem derivWithin_tsum {ι : Type u_1} {F : Type u_2} {E : Type u_3} [NontriviallyNormedField E] [IsRCLikeNormedField E] [NormedAddCommGroup F] [NormedSpace E F] {s : Set E} {f : ι → E → F} (hs : IsOpen s) {x : E} (hx : x ∈ s) (hf : ∀ y ∈ s, Summable fun (n : ι) => f n y) (h : SummableLocallyUniformlyOn (fun (n : ι) => derivWithin (fun (z : E) => f n z) s) s) (hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt E (f n) r) : derivWithin (fun (z : E) => ∑' (n : ι), f n z) s x = ∑' (n : ι), derivWithin (f n) s x

The derivWithin of a sum whose derivative is absolutely and uniformly convergent sum on an open set s is the sum of the derivatives of sequence of functions on the open set s

theorem iteratedDerivWithin_tsum {ι : Type u_1} {F : Type u_2} {E : Type u_3} [NontriviallyNormedField E] [IsRCLikeNormedField E] [NormedAddCommGroup F] [NormedSpace E F] {s : Set E} {f : ι → E → F} (m : ℕ) (hs : IsOpen s) {x : E} (hx : x ∈ s) (hsum : ∀ t ∈ s, Summable fun (n : ι) => f n t) (h : ∀ (k : ℕ), 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun (n : ι) => iteratedDerivWithin k (fun (z : E) => f n z) s) s) (hf2 : ∀ (n : ι) (k : ℕ) (r : E), k ≤ m → r ∈ s → DifferentiableAt E (iteratedDerivWithin k (fun (z : E) => f n z) s) r) : iteratedDerivWithin m (fun (z : E) => ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x

If a sequence of functions fₙ is such that ∑ fₙ (z) is summable for each z in an open set s, and for each 1 ≤ k ≤ m, the series of k-th iterated derivatives ∑ (iteratedDerivWithin k fₙ s) (z) is summable locally uniformly on s, and each fₙ is m-times differentiable, then the m-th iterated derivative of the sum is the sum of the m-th iterated derivatives.