feat(Analysis/NormedSpace/FunctionSeries): Add SummableUniformlyOn ve…

Mathlib/Analysis/NormedSpace/FunctionSeries.lean

@@ -3,8 +3,8 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Analysis.Normed.Group.InfiniteSum
-import Mathlib.Topology.Instances.ENNReal.Lemmas
+import Mathlib.Analysis.Calculus.UniformLimitsDeriv
+import Mathlib.Topology.Algebra.InfiniteSum.UniformOn
 
 /-!
 # Continuity of series of functions
@@ -36,6 +36,10 @@ theorem tendstoUniformlyOn_tsum {f : α → β → F} (hu : Summable u) {s : Set
   apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
   exact (A.subtype _).tsum_le_tsum (fun n => hfu _ _ hx) (hu.subtype _)
 
+theorem HasSumUniformlyOn_of_bounded {f : α → β → F} (hu : Summable u) {s : Set β}
+    (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) : HasSumUniformlyOn f (fun x => ∑' n, f n x) {s} :=  by
+  simp [hasSumUniformlyOn_iff_tendstoUniformlyOn, tendstoUniformlyOn_tsum hu hfu]
+
 /-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
 Version relative to a set, with index set `ℕ`. -/
 theorem tendstoUniformlyOn_tsum_nat {f : ℕ → β → F} {u : ℕ → ℝ} (hu : Summable u) {s : Set β}
@@ -72,6 +76,12 @@ theorem tendstoUniformlyOn_tsum_of_cofinite_eventually {ι : Type*} {f : ι →
   have : ¬ i ∈ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
   aesop
 
+theorem HasSumUniformlyOn_of_cofinite_eventually {ι : Type*} {f : ι → β → F} {u : ι → ℝ}
+    (hu : Summable u) {s : Set β} (hfu : ∀ᶠ n in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n) :
+    HasSumUniformlyOn f (fun x => ∑' n, f n x) {s} := by
+  simp [hasSumUniformlyOn_iff_tendstoUniformlyOn,
+    tendstoUniformlyOn_tsum_of_cofinite_eventually hu hfu]
+
 theorem tendstoUniformlyOn_tsum_nat_eventually {α F : Type*} [NormedAddCommGroup F]
     [CompleteSpace F] {f : ℕ → α → F} {u : ℕ → ℝ} (hu : Summable u) {s : Set α}
     (hfu : ∀ᶠ n in atTop, ∀ x ∈ s, ‖f n x‖ ≤ u n) :
@@ -120,3 +130,34 @@ theorem continuous_tsum [TopologicalSpace β] {f : α → β → F} (hf : ∀ i,
     (hu : Summable u) (hfu : ∀ n x, ‖f n x‖ ≤ u n) : Continuous fun x => ∑' n, f n x := by
   simp_rw [continuous_iff_continuousOn_univ] at hf ⊢
   exact continuousOn_tsum hf hu fun n x _ => hfu n x
+
+lemma SummableLocallyUniformlyOn.of_locally_bounded [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 := by
+  apply HasSumLocallyUniformlyOn.summableLocallyUniformlyOn (g := (fun x => ∑' i, f i x))
+  rw [hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn,
+    tendstoLocallyUniformlyOn_iff_forall_isCompact hs]
+  intro K hK hKc
+  obtain ⟨u, hu1, hu2⟩ := hu K hK hKc
+  apply tendstoUniformlyOn_tsum hu1 fun n x hx ↦ hu2 n ⟨x, hx⟩
+
+theorem derivWithin_tsum {F E : Type*} [NontriviallyNormedField E] [IsRCLikeNormedField E]
+    [NormedField F] [NormedSpace E F] (f : α → E → F) {s : Set E}
+    (hs : IsOpen s) {x : E} (hx : x ∈ s) (hf : ∀ y ∈ s, Summable fun n ↦ f n y)
+    (h : SummableLocallyUniformlyOn (fun n ↦ (derivWithin (fun z ↦ f n z) s)) s)
+    (hf2 : ∀ n r, r ∈ s → DifferentiableAt E (f n) r) :
+    derivWithin (fun z ↦ ∑' n , f n z) s x = ∑' n, derivWithin (fun z ↦ f n z) s x := by
+  apply HasDerivWithinAt.derivWithin ?_ (IsOpen.uniqueDiffWithinAt hs hx)
+  apply HasDerivAt.hasDerivWithinAt
+  apply hasDerivAt_of_tendstoLocallyUniformlyOn hs _ _ (fun y hy ↦ Summable.hasSum (hf y hy)) hx
+  · use fun n : Finset α ↦ fun a ↦ ∑ i ∈ n, derivWithin (fun z ↦ f i z) s a
+  · obtain ⟨g, hg⟩ := h
+    apply (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).congr_right
+    exact fun ⦃b⦄ hb ↦ Eq.symm (HasSumLocallyUniformlyOn.tsum_eqOn hg hb)
+  · filter_upwards with t r hr
+    apply HasDerivAt.sum
+    intro q hq
+    apply HasDerivWithinAt.hasDerivAt
+    · exact DifferentiableWithinAt.hasDerivWithinAt (hf2 q r hr).differentiableWithinAt
+    · exact IsOpen.mem_nhds hs hr