Infinite sums in (semi)normed groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 in 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, has_sum.norm_le_of_bounded: if ‖f i‖ ≤ g i, where ∑' i, g i is a summable series, then ‖∑' i, f i‖ ≤ ∑' i, g i.

Tags #

infinite series, absolute convergence, normed group

theorem cauchy_seq_finset_iff_vanishing_norm {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} :

cauchy_seq (λ (s : finset ι), s.sum (λ (i : ι), f i)) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (s : finset ι), ∀ (t : finset ι), disjoint t s → ‖t.sum (λ (i : ι), f i)‖ < ε)

source

theorem summable_iff_vanishing_norm {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] [complete_space E] {f : ι → E} :

summable f ↔ ∀ (ε : ℝ), ε > 0 → (∃ (s : finset ι), ∀ (t : finset ι), disjoint t s → ‖t.sum (λ (i : ι), f i)‖ < ε)

source

theorem cauchy_seq_finset_of_norm_bounded_eventually {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} {g : ι → ℝ} (hg : summable g) (h : ∀ᶠ (i : ι) in filter.cofinite , ‖f i‖ ≤ g i) :

cauchy_seq (λ (s : finset ι), s.sum (λ (i : ι), f i))

source

theorem cauchy_seq_finset_of_norm_bounded {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} (g : ι → ℝ) (hg : summable g) (h : ∀ (i : ι), ‖f i‖ ≤ g i) :

cauchy_seq (λ (s : finset ι), s.sum (λ (i : ι), f i))

source

theorem cauchy_seq_range_of_norm_bounded {E : Type u_3} [seminormed_add_comm_group E] {f : ℕ → E} (g : ℕ → ℝ) (hg : cauchy_seq (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), g i))) (hf : ∀ (i : ℕ), ‖f i‖ ≤ g i) :

cauchy_seq (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i))

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

source

theorem cauchy_seq_finset_of_summable_norm {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} (hf : summable (λ (a : ι), ‖f a‖)) :

cauchy_seq (λ (s : finset ι), s.sum (λ (a : ι), f a))

source

theorem has_sum_of_subseq_of_summable {ι : Type u_1} {α : Type u_2} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} (hf : summable (λ (a : ι), ‖f a‖)) {s : α → finset ι} {p : filter α} [p.ne_bot] (hs : filter.tendsto s p filter.at_top) {a : E} (ha : filter.tendsto (λ (b : α), (s b).sum (λ (i : ι), f i)) p (nhds a)) :

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

source

theorem has_sum_iff_tendsto_nat_of_summable_norm {E : Type u_3} [seminormed_add_comm_group E] {f : ℕ → E} {a : E} (hf : summable (λ (i : ℕ), ‖f i‖)) :

has_sum f a ↔ filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), f i)) filter.at_top (nhds a)

source

theorem summable_of_norm_bounded {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] [complete_space 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.

source

theorem has_sum.norm_le_of_bounded {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} {g : ι → ℝ} {a : E} {b : ℝ} (hf : has_sum f a) (hg : has_sum g b) (h : ∀ (i : ι), ‖f i‖ ≤ g i) :

‖a‖ ≤ b

source

theorem tsum_of_norm_bounded {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} {g : ι → ℝ} {a : ℝ} (hg : has_sum 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.

source

theorem norm_tsum_le_tsum_norm {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} (hf : summable (λ (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.

source

theorem tsum_of_nnnorm_bounded {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} {g : ι → nnreal} {a : nnreal} (hg : has_sum 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.

source

theorem nnnorm_tsum_le {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] {f : ι → E} (hf : summable (λ (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.

source

theorem summable_of_norm_bounded_eventually {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] [complete_space 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.

source

theorem summable_of_nnnorm_bounded {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] [complete_space E] {f : ι → E} (g : ι → nnreal) (hg : summable g) (h : ∀ (i : ι), ‖f i‖₊ ≤ g i) :

summable f

source

theorem summable_of_summable_norm {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] [complete_space E] {f : ι → E} (hf : summable (λ (a : ι), ‖f a‖)) :

summable f

source

theorem summable_of_summable_nnnorm {ι : Type u_1} {E : Type u_3} [seminormed_add_comm_group E] [complete_space E] {f : ι → E} (hf : summable (λ (a : ι), ‖f a‖₊)) :

summable f