English
A function f is summable with respect to L if and only if its mapped sum to the completion is summable and the completion sum lies in the image of toCompl.
Русский
Функция f суммируема по L тогда и только тогда, когда сумма в дополнении к ней по toCompl суммируема и её сумма лежит в образе toCompl.
LaTeX
$$$$ \text{Summable } f\ L \iff \Big( \text{Summable } (toCompl \circ f)\ L \wedge \sum'[L] i, toCompl (f i) \in \operatorname{range} toCompl \Big). $$$$
Lean4
/-- 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_iff_cauchySeq_finset_and_tsum_mem (f : β → α) :
Summable f ↔ CauchySeq (fun s : Finset β ↦ ∑ b ∈ s, f b) ∧ ∑' i, toCompl (f i) ∈ Set.range toCompl := by
classical
constructor
· rintro ⟨a, ha⟩
exact ⟨ha.cauchySeq, ((summable_iff_summable_compl_and_tsum_mem f).mp ⟨a, ha⟩).2⟩
· rintro ⟨h_cauchy, h_tsum⟩
apply (summable_iff_summable_compl_and_tsum_mem f).mpr
constructor
· apply summable_iff_cauchySeq_finset.mpr
simp_rw [Function.comp_apply, ← map_sum]
exact h_cauchy.map (uniformContinuous_coe α)
· exact h_tsum
