Continuity of series of functions

We show that series of functions are continuous when each individual function in the series is and additionally suitable uniform summable bounds are satisfied, in continuous_tsum.

For smoothness of series of functions, see the file Analysis.Calculus.SmoothSeries.

theorem tendstoUniformlyOn_tsum {α : 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) : TendstoUniformlyOn (fun (t : Finset α) (x : β) => ∑ n ∈ t, f n x) (fun (x : β) => ∑' (n : α), f n x) Filter.atTop s

An infinite sum of functions with summable sup norm is the uniform limit of its partial sums. Version relative to a set, with general index set.

theorem tendstoUniformlyOn_tsum_nat {β : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [CompleteSpace F] {f : ℕ → β → F} {u : ℕ → ℝ} (hu : Summable u) {s : Set β} (hfu : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ u n) : TendstoUniformlyOn (fun (N : ℕ) (x : β) => ∑ n ∈ Finset.range N, f n x) (fun (x : β) => ∑' (n : ℕ), f n x) Filter.atTop s

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_of_cofinite_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) : TendstoUniformlyOn (fun (t : Finset ι) (x : β) => ∑ n ∈ t, f n x) (fun (x : β) => ∑' (n : ι), f n x) Filter.atTop s

An infinite sum of functions with eventually summable sup norm is the uniform limit of its partial sums. Version relative to a set, with general index set.

theorem tendstoUniformly_tsum {α : Type u_1} {β : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} {f : α → β → F} (hu : Summable u) (hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n) : TendstoUniformly (fun (t : Finset α) (x : β) => ∑ n ∈ t, f n x) (fun (x : β) => ∑' (n : α), f n x) Filter.atTop

An infinite sum of functions with summable sup norm is the uniform limit of its partial sums. Version with general index set.

theorem tendstoUniformly_tsum_nat {β : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [CompleteSpace F] {f : ℕ → β → F} {u : ℕ → ℝ} (hu : Summable u) (hfu : ∀ (n : ℕ) (x : β), ‖f n x‖ ≤ u n) : TendstoUniformly (fun (N : ℕ) (x : β) => ∑ n ∈ Finset.range N, f n x) (fun (x : β) => ∑' (n : ℕ), f n x) Filter.atTop

An infinite sum of functions with summable sup norm is the uniform limit of its partial sums. Version with index set ℕ.

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

An infinite sum of functions with eventually summable sup norm is the uniform limit of its partial sums. Version with general index set.

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

An infinite sum of functions with summable sup norm is continuous on a set if each individual function is.

theorem continuous_tsum {α : Type u_1} {β : Type u_2} {F : Type u_3} [NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [TopologicalSpace β] {f : α → β → F} (hf : ∀ (i : α), Continuous (f i)) (hu : Summable u) (hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n) : Continuous fun (x : β) => ∑' (n : α), f n x

An infinite sum of functions with summable sup norm is continuous if each individual function is.