Documentation

Mathlib.Analysis.NormedSpace.FunctionSeries

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 : α), xs, f n x u n) :
TendstoUniformlyOn (fun (t : Finset α) (x : β) => nt, 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 : ), xs, f n x u n) :
TendstoUniformlyOn (fun (N : ) (x : β) => nFinset.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 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 : β) => nt, 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 : β) => nFinset.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 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 : α), 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} [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.