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 and NormedAddCommGroup.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) : ∃ (f : ℕ → ℕ), StrictMono f ∧ Summable fun (i : ℕ) => dist (u (f (i + 1))) (u (f i))

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)) : CompleteSpace E

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.