Infinite sums in the completion of a topological group

theorem hasSum_iff_hasSum_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {L : SummationFilter β} (f : β → α) (a : α) : HasSum (⇑UniformSpace.Completion.toCompl ∘ f) (↑a) L ↔ HasSum f a L

A function f has a sum in a uniform additive group α if and only if it has that sum in the completion of α.

theorem summable_iff_summable_compl_and_tsum_mem {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {L : SummationFilter β} (f : β → α) : Summable f L ↔ Summable (⇑UniformSpace.Completion.toCompl ∘ f) L ∧ ∑'[L] (i : β), UniformSpace.Completion.toCompl (f i) ∈ Set.range ⇑UniformSpace.Completion.toCompl

A function f is summable in a uniform additive group α if and only if it is summable in Completion α and its sum in Completion α lies in the range of toCompl : α →+ Completion α.

theorem summable_iff_cauchySeq_finset_and_tsum_mem {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] (f : β → α) : Summable f ↔ (CauchySeq fun (s : Finset β) => ∑ b ∈ s, f b) ∧ ∑' (i : β), UniformSpace.Completion.toCompl (f i) ∈ Set.range ⇑UniformSpace.Completion.toCompl

A function f is summable in a uniform additive group α if and only if the net of its partial sums is Cauchy and its sum in Completion α lies in the range of toCompl : α →+ Completion α. (The condition that the net of partial sums is Cauchy can be checked using cauchySeq_finset_iff_sum_vanishing or cauchySeq_finset_iff_tsum_vanishing.)

theorem Summable.toCompl_tsum {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {L : SummationFilter β} [L.NeBot] {f : β → α} (hf : Summable f L) : ∑'[L] (i : β), UniformSpace.Completion.toCompl (f i) = ↑(∑'[L] (i : β), f i)

If a function f is summable in a uniform additive group α, then its sum in α is the same as its sum in Completion α.