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 #
- [BL76]
NormedAddCommGroup.completeSpace_of_summable_imp_tendsto
andNormedAddCommGroup.summable_imp_tendsto_of_complete
correspond 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 : ℕ) => ∑ i ∈ Finset.range n, 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 : ℕ) => ∑ i ∈ Finset.range n, 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 : ℕ) => ∑ i ∈ Finset.range n, 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.