[Merged by Bors] - feat: characterize summability by vanishing of tsums

[alreadydone]

---

Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Tail.20estimate.20for.20abs.2E.20convergent.20series/near/400324559

[MichaelStollBayreuth]

LGTM!

[sgouezel]

The direct implication in your theorem does require completeness, right? And in general the right hand side is equivalent to the fact that the sum over finsets is a Cauchy sequence, if I understand correctly. Could you give a statement like this, modelled on cauchySeq_finset_iff_vanishing, and then deduce your result in the complete case? Same thing for next theorem.

[alreadydone]

You mean it doesn't require completeness, right? I can indeed remove the completeness assumption in the forward implications, even UniformAddGroup; only TopologicalAddGroup is required, and I've generalized tendsto_tsum_compl_atTop_zero to remove uniformity and golfed it using my theorem. However, I don't think I can state my theorems using cauchySeq, or even fit the two theorems into the filter framework, since I'm dealing with tsums over general Sets (not necessarily Finsets or complement of Finsets); we certainly can't use atTop on Set α and have to introduce some other filter.

[sgouezel]

I wasn't clear, sorry. I am asking if the following is true:

theorem foobar {f : α → G} : (CauchySeq fun s : Finset β => ∑ b in s, f b) ↔
    ∀ e ∈ 𝓝 (0 : G), ∃ s : Finset α, ∀ t : Set α, Disjoint t s → (∑' a : t, f a) ∈ e

[alreadydone]

Sorry for the misunderstanding! Your approach indeed looks much nicer. I removed the summable_iff_... versions since they follow easily from the cauchySeq_finset_iff_... versions and summable_iff_cauchySeq_finset when the uniform group is complete, and since the reverse implication isn't very useful; summable_iff_vanishing will always be easier to verify.

[sgouezel]

Thanks! Could you also give a version of summable_iff_vanishing with your phrasing (probably summable_iff_tsum_vanishing)?
bors d+

[mathlib-bors]

✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[alreadydone]

Thanks! Could you also give a version of summable_iff_vanishing with your phrasing (probably summable_iff_tsum_vanishing)? bors d+

I removed them in this commit (see this comment for the rationale), but it should be easy to add back the CompleteUniformAddGroup section.

[sgouezel]

Yes, I've seen that, but I think it's good to have it for coherence.

[sgouezel]

Or remove also summable_iff_vanishing. But having one and not the other is strange.

[alreadydone]

@sgouezel I diagnosed the slowness to be due to DecidableEq instance mismatch. Do you think I should add [DecidableEq β] to summable_iff_cauchySeq_finset etc.?

Update: commited; let's see if CI is happy. I can revert it if you don't like it for some reason.

It's a bit surprising that refine worked despite the instance mismatch; a Lean 4 feature?

[alreadydone]

It's a bit surprising that refine worked despite the instance mismatch; a Lean 4 feature?

Actually I think it's because CauchySeq actually only needs Preorder to work (for atTop to make sense), which is independent of the DecidableEq instance; it also explains why refine is slow, as Lean needs to unfold to the Preorder. We can probably get rid of some DecidableEq added here once we do the refactor there.

[alreadydone]

Thanks!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Check all files imported
• Lint style
• Build