mathlib documentation

analysis.normed.group.infinite_sum

Infinite sums in (semi)normed groups #

In a complete (semi)normed group,

Tags #

infinite series, absolute convergence, normed group

theorem cauchy_seq_finset_iff_vanishing_norm {ι : Type u_1} {E : Type u_3} [semi_normed_group E] {f : ι → E} :
cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i) ∀ (ε : ), ε > 0(∃ (s : finset ι), ∀ (t : finset ι), disjoint t s∑ (i : ι) in t, f i < ε)
theorem summable_iff_vanishing_norm {ι : Type u_1} {E : Type u_3} [semi_normed_group E] [complete_space E] {f : ι → E} :
summable f ∀ (ε : ), ε > 0(∃ (s : finset ι), ∀ (t : finset ι), disjoint t s∑ (i : ι) in t, f i < ε)
theorem cauchy_seq_finset_of_norm_bounded_eventually {ι : Type u_1} {E : Type u_3} [semi_normed_group E] {f : ι → E} {g : ι → } (hg : summable g) (h : ∀ᶠ (i : ι) in filter.cofinite, f i g i) :
cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i)
theorem cauchy_seq_finset_of_norm_bounded {ι : Type u_1} {E : Type u_3} [semi_normed_group E] {f : ι → E} (g : ι → ) (hg : summable g) (h : ∀ (i : ι), f i g i) :
cauchy_seq (λ (s : finset ι), ∑ (i : ι) in s, f i)
theorem cauchy_seq_finset_of_summable_norm {ι : Type u_1} {E : Type u_3} [semi_normed_group E] {f : ι → E} (hf : summable (λ (a : ι), f a)) :
cauchy_seq (λ (s : finset ι), ∑ (a : ι) in s, f a)
theorem has_sum_of_subseq_of_summable {ι : Type u_1} {α : Type u_2} {E : Type u_3} [semi_normed_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 : α), ∑ (i : ι) in s b, f i) p (𝓝 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 has_sum_iff_tendsto_nat_of_summable_norm {E : Type u_3} [semi_normed_group E] {f : → E} {a : E} (hf : summable (λ (i : ), f i)) :
has_sum f a filter.tendsto (λ (n : ), ∑ (i : ) in finset.range n, f i) filter.at_top (𝓝 a)
theorem summable_of_norm_bounded {ι : Type u_1} {E : Type u_3} [semi_normed_group E] [complete_space 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 has_sum.norm_le_of_bounded {ι : Type u_1} {E : Type u_3} [semi_normed_group E] {f : ι → E} {g : ι → } {a : E} {b : } (hf : has_sum f a) (hg : has_sum g b) (h : ∀ (i : ι), f i g i) :
theorem tsum_of_norm_bounded {ι : Type u_1} {E : Type u_3} [semi_normed_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.

theorem norm_tsum_le_tsum_norm {ι : Type u_1} {E : Type u_3} [semi_normed_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.

theorem tsum_of_nnnorm_bounded {ι : Type u_1} {E : Type u_3} [semi_normed_group E] {f : ι → E} {g : ι → ℝ≥0} {a : ℝ≥0} (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.

theorem nnnorm_tsum_le {ι : Type u_1} {E : Type u_3} [semi_normed_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.

theorem summable_of_norm_bounded_eventually {ι : Type u_1} {E : Type u_3} [semi_normed_group E] [complete_space 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} [semi_normed_group E] [complete_space E] {f : ι → E} (g : ι → ℝ≥0) (hg : summable g) (h : ∀ (i : ι), f i∥₊ g i) :
theorem summable_of_summable_norm {ι : Type u_1} {E : Type u_3} [semi_normed_group E] [complete_space E] {f : ι → E} (hf : summable (λ (a : ι), f a)) :
theorem summable_of_summable_nnnorm {ι : Type u_1} {E : Type u_3} [semi_normed_group E] [complete_space E] {f : ι → E} (hf : summable (λ (a : ι), f a∥₊)) :