# 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`.

TODO: update this to use `SummableUniformlyOn`.

source
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.

source
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 `ℕ`.

source
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.

source
theorem tendstoUniformlyOn_tsum_nat_eventually {α : Type u_4} {F : Type u_5} [NormedAddCommGroup F] [CompleteSpace F] {f : ℕ → α → F} {u : ℕ → ℝ} (hu : Summable u) {s : Set α} (hfu : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ 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
source
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.

source
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 `ℕ`.

source
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.

source
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.

source
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.