Completeness of normed groups #
This file includes a completeness criterion for normed additive groups in terms of convergent series.
Main results #
NormedAddCommGroup.completeSpace_of_summable_imp_tendsto: A normed additive group is complete if any absolutely convergent series converges in the space.
References #
- [bergh_lofstrom_1976]
NormedAddCommGroup.completeSpace_of_summable_imp_tendstoandNormedAddCommGroup.summable_imp_tendsto_of_completecorrespond to the two directions of Lemma 2.2.1.
Tags #
CompleteSpace, CauchySeq
theorem
Metric.exists_subseq_summable_dist_of_cauchySeq
{α : Type u_1}
[PseudoMetricSpace α]
(u : ℕ → α)
(hu : CauchySeq u)
:
theorem
NormedAddCommGroup.completeSpace_of_summable_imp_tendsto
{E : Type u_1}
[NormedAddCommGroup E]
(h : ∀ (u : ℕ → E),
(Summable fun (x : ℕ) => ‖u x‖) →
∃ (a : E), Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range n) fun (i : ℕ) => u i) Filter.atTop (nhds a))
:
A normed additive group is complete if any absolutely convergent series converges in the space.
theorem
NormedAddCommGroup.summable_imp_tendsto_of_complete
{E : Type u_1}
[NormedAddCommGroup E]
[CompleteSpace E]
(u : ℕ → E)
(hu : Summable fun (x : ℕ) => ‖u x‖)
:
∃ (a : E), Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range n) fun (i : ℕ) => u i) Filter.atTop (nhds a)
In a complete normed additive group, every absolutely convergent series converges in the space.
theorem
NormedAddCommGroup.summable_imp_tendsto_iff_completeSpace
{E : Type u_1}
[NormedAddCommGroup E]
:
(∀ (u : ℕ → E),
(Summable fun (x : ℕ) => ‖u x‖) →
∃ (a : E), Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range n) fun (i : ℕ) => u i) Filter.atTop (nhds a)) ↔ CompleteSpace E
In a normed additive group, every absolutely convergent series converges in the space iff the space is complete.