Documentation

Mathlib.Analysis.Normed.Group.Completeness

Completeness of normed groups #

This file includes a completeness criterion for normed additive groups in terms of convergent series.

Main results #

References #

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 : ) => 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.