# 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} [] {u : α} {f : αβF} (hu : ) {s : Set β} (hfu : ∀ (n : α), xs, f n x u n) :
TendstoUniformlyOn (fun (t : ) (x : β) => Finset.sum t fun (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 general index set.

theorem tendstoUniformlyOn_tsum_nat {β : Type u_2} {F : Type u_3} [] {f : βF} {u : } (hu : ) {s : Set β} (hfu : ∀ (n : ), xs, f n x u n) :
TendstoUniformlyOn (fun (N : ) (x : β) => Finset.sum () fun (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 tendstoUniformly_tsum {α : Type u_1} {β : Type u_2} {F : Type u_3} [] {u : α} {f : αβF} (hu : ) (hfu : ∀ (n : α) (x : β), f n x u n) :
TendstoUniformly (fun (t : ) (x : β) => Finset.sum t fun (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 general index set.

theorem tendstoUniformly_tsum_nat {β : Type u_2} {F : Type u_3} [] {f : βF} {u : } (hu : ) (hfu : ∀ (n : ) (x : β), f n x u n) :
TendstoUniformly (fun (N : ) (x : β) => Finset.sum () fun (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 continuousOn_tsum {α : Type u_1} {β : Type u_2} {F : Type u_3} [] {u : α} [] {f : αβF} {s : Set β} (hf : ∀ (i : α), ContinuousOn (f i) s) (hu : ) (hfu : ∀ (n : α), xs, 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} [] {u : α} [] {f : αβF} (hf : ∀ (i : α), Continuous (f i)) (hu : ) (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.