Documentation

Mathlib.Analysis.Normed.Group.InfiniteSum

Infinite sums in (semi)normed groups #

In a complete (semi)normed group,

Tags #

infinite series, absolute convergence, normed group

theorem cauchySeq_finset_iff_vanishing_norm {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} :
(CauchySeq fun s => Finset.sum s fun i => f i) ∀ (ε : ), ε > 0s, ∀ (t : Finset ι), Disjoint t sFinset.sum t fun i => f i < ε
theorem summable_iff_vanishing_norm {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ιE} :
Summable f ∀ (ε : ), ε > 0s, ∀ (t : Finset ι), Disjoint t sFinset.sum t fun i => f i < ε
theorem cauchySeq_finset_of_norm_bounded_eventually {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} {g : ι} (hg : Summable g) (h : ∀ᶠ (i : ι) in Filter.cofinite, f i g i) :
CauchySeq fun s => Finset.sum s fun i => f i
theorem cauchySeq_finset_of_norm_bounded {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} (g : ι) (hg : Summable g) (h : ∀ (i : ι), f i g i) :
CauchySeq fun s => Finset.sum s fun i => f i
theorem cauchySeq_range_of_norm_bounded {E : Type u_3} [SeminormedAddCommGroup E] {f : E} (g : ) (hg : CauchySeq fun n => Finset.sum (Finset.range n) fun i => g i) (hf : ∀ (i : ), f i g i) :
CauchySeq fun n => Finset.sum (Finset.range n) fun i => f i

A version of the direct comparison test for conditionally convergent series. See cauchySeq_finset_of_norm_bounded for the same statement about absolutely convergent ones.

theorem cauchySeq_finset_of_summable_norm {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} (hf : Summable fun a => f a) :
CauchySeq fun s => Finset.sum s fun a => f a
theorem hasSum_of_subseq_of_summable {ι : Type u_1} {α : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} (hf : Summable fun a => f a) {s : αFinset ι} {p : Filter α} [Filter.NeBot p] (hs : Filter.Tendsto s p Filter.atTop) {a : E} (ha : Filter.Tendsto (fun b => Finset.sum (s b) fun i => f i) p (nhds a)) :
HasSum f a

If a function f is summable in norm, and along some sequence of finsets exhausting the space its sum is converging to a limit a, then this holds along all finsets, i.e., f is summable with sum a.

theorem hasSum_iff_tendsto_nat_of_summable_norm {E : Type u_3} [SeminormedAddCommGroup E] {f : E} {a : E} (hf : Summable fun i => f i) :
HasSum f a Filter.Tendsto (fun n => Finset.sum (Finset.range n) fun i => f i) Filter.atTop (nhds a)
theorem summable_of_norm_bounded {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ιE} (g : ι) (hg : Summable g) (h : ∀ (i : ι), f i g i) :

The direct comparison test for series: if the norm of f is bounded by a real function g which is summable, then f is summable.

theorem HasSum.norm_le_of_bounded {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} {g : ι} {a : E} {b : } (hf : HasSum f a) (hg : HasSum g b) (h : ∀ (i : ι), f i g i) :
theorem tsum_of_norm_bounded {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} {g : ι} {a : } (hg : HasSum g a) (h : ∀ (i : ι), f i g i) :
∑' (i : ι), f i a

Quantitative result associated to the direct comparison test for series: If ∑' i, g i is summable, and for all i, ‖f i‖ ≤ g i, then ‖∑' i, f i‖ ≤ ∑' i, g i. Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem norm_tsum_le_tsum_norm {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} (hf : Summable fun i => f i) :
∑' (i : ι), f i ∑' (i : ι), f i

If ∑' i, ‖f i‖ is summable, then ‖∑' i, f i‖ ≤ (∑' i, ‖f i‖). Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem tsum_of_nnnorm_bounded {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} {g : ιNNReal} {a : NNReal} (hg : HasSum g a) (h : ∀ (i : ι), f i‖₊ g i) :
∑' (i : ι), f i‖₊ a

Quantitative result associated to the direct comparison test for series: If ∑' i, g i is summable, and for all i, ‖f i‖₊ ≤ g i, then ‖∑' i, f i‖₊ ≤ ∑' i, g i. Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem nnnorm_tsum_le {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ιE} (hf : Summable fun i => f i‖₊) :
∑' (i : ι), f i‖₊ ∑' (i : ι), f i‖₊

If ∑' i, ‖f i‖₊ is summable, then ‖∑' i, f i‖₊ ≤ ∑' i, ‖f i‖₊. Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

theorem summable_of_norm_bounded_eventually {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ιE} (g : ι) (hg : Summable g) (h : ∀ᶠ (i : ι) in Filter.cofinite, f i g i) :

Variant of the direct comparison test for series: if the norm of f is eventually bounded by a real function g which is summable, then f is summable.

theorem summable_of_nnnorm_bounded {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ιE} (g : ιNNReal) (hg : Summable g) (h : ∀ (i : ι), f i‖₊ g i) :
theorem summable_of_summable_norm {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ιE} (hf : Summable fun a => f a) :
theorem summable_of_summable_nnnorm {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ιE} (hf : Summable fun a => f a‖₊) :