Infinite sums in the completion of a topological group #
theorem
hasSum_iff_hasSum_compl
{α : Type u_1}
{β : Type u_2}
[AddCommGroup α]
[UniformSpace α]
[UniformAddGroup α]
(f : β → α)
(a : α)
:
A function f has a sum in an 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 α]
[UniformAddGroup α]
(f : β → α)
:
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 α]
[UniformAddGroup α]
(f : β → α)
:
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 α]
[UniformAddGroup α]
{f : β → α}
(hf : Summable f)
:
∑' (i : β), UniformSpace.Completion.toCompl (f i) = ↑α (∑' (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 α.