Infinite sums in (semi)normed groups

In a complete (semi)normed group,

• summable_iff_vanishing_norm: a series ∑' i, f i is summable if and only if for any ε > 0, there exists a finite set s such that the sum ∑ i ∈ t, f i over any finite set t disjoint with s has norm less than ε;

• Summable.of_norm_bounded, Summable.of_norm_bounded_eventually: if ‖f i‖ is bounded above by a summable series ∑' i, g i, then ∑' i, f i is summable as well; the same is true if the inequality hold only off some finite set.

• tsum_of_norm_bounded, HasSum.norm_le_of_bounded: if ‖f i‖ ≤ g i, where ∑' i, g i is a summable series, then ‖∑' i, f i‖ ≤ ∑' i, g i.

• versions of these lemmas for nnnorm and enorm.

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 ι) => ∑ i ∈ s, f i) ↔ ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

theorem summable_iff_vanishing_norm {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} : Summable f ↔ ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, 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 ι) => ∑ i ∈ s, 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 ι) => ∑ i ∈ s, f i

theorem cauchySeq_range_of_norm_bounded {E : Type u_3} [SeminormedAddCommGroup E] {f : ℕ → E} {g : ℕ → ℝ} (hg : CauchySeq fun (n : ℕ) => ∑ i ∈ Finset.range n, g i) (hf : ∀ (i : ℕ), ‖f i‖ ≤ g i) : CauchySeq fun (n : ℕ) => ∑ i ∈ Finset.range n, 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 ι) => ∑ a ∈ s, 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 α} [p.NeBot] (hs : Filter.Tendsto s p Filter.atTop) {a : E} (ha : Filter.Tendsto (fun (b : α) => ∑ i ∈ s b, 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 : ℕ) => ∑ i ∈ Finset.range n, 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) : Summable f

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.enorm_le_of_bounded {ι : Type u_1} {ε : Type u_5} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] {f : ι → ε} {g : ι → ENNReal} {a : ε} {b : ENNReal} (hf : HasSum f a) (hg : HasSum g b) (h : ∀ (i : ι), ‖f i‖ₑ ≤ g i) : ‖a‖ₑ ≤ b

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) : ‖a‖ ≤ b

theorem tsum_of_enorm_bounded {ι : Type u_1} {ε : Type u_5} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] {f : ι → ε} {g : ι → ENNReal} {a : ENNReal} (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, 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 enorm_tsum_le_tsum_enorm {ι : Type u_1} {ε : Type u_5} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] {f : ι → ε} : ‖∑' (i : ι), f i‖ₑ ≤ ∑' (i : ι), ‖f 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) : Summable f

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_norm_bounded_eventually_nat {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ℕ → E} {g : ℕ → ℝ} (hg : Summable g) (h : ∀ᶠ (i : ℕ) in Filter.atTop, ‖f i‖ ≤ g i) : Summable f

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) : Summable f

theorem Summable.of_norm {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} (hf : Summable fun (a : ι) => ‖f a‖) : Summable f

theorem Summable.of_nnnorm {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} (hf : Summable fun (a : ι) => ‖f a‖₊) : Summable f