Sum of `ENat` (`ℕ∞`)

Stream: Is there code for X?

[Markus Schmaus]

I have a function f : ℕ → ℕ∞, and would like functions for the partial sums, the infinite sum, as well as theorems about how they relate to each other. I found docs#tsum , but this seems to leave the question of existences and uniqueness of the sum unresolved. And I can't find anything on partial sums. What's the easiest approach to this?

[Ruben Van de Velde]

@loogle tsum, ENat

[loogle]

:search: contDiff_tsum, contDiff_tsum_of_eventually, and 2 more

[Ruben Van de Velde]

That's not very encouraging

[Sébastien Gouëzel]

Yes, we have a lot of material for functions taking values in ENNReal (i.e., non negative reals with added infinity), but not so much for functions taking values in ENat, simply because no-one has needed them until then. You could try to mimick the statements for ENNReal (for instance what is around docs#ENNReal.summable)

[Josha Dekker]

But can't you just coerce it to ENNReal and use the results there? By using something like https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Data/Real/ENatENNReal.lean#L29-L29?

[Ruben Van de Velde]

Coercing seems worth trying, but I'm not sure that'll be much easier

[Jireh Loreaux]

I'm confused. @Markus Schmaus you don't really mean the infinite sum of a sequence in ENat, do you? This will be finite if and only if the partial sums are eventually constant if and only if the sequence is eventually zero, and hence in that case the infinite sum is really just a finite sum in disguise.

[Markus Schmaus]

I mean an infinite sum in ENat, which quite likely may be infinite, which is fine for ENat, or may be finite if the sequence is eventually zero.

For context, I'm interested in the length of concatenating a potentially infinite list of potentially infinite iterators.

[Markus Schmaus]

I will look into ENNReal.

[Mitchell Lee]

Just take the sum using tsum. What do you need to prove about it?

[Mitchell Lee]

(Also, use the sigma notation for tsum)

[Mitchell Lee]

This page might have some of the theorems you want: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/InfiniteSum/NatInt.html

[Mitchell Lee]

To be more clear, for f : ℕ → ℕ∞, if you write open scoped BigOperators:

The sum $\sum_{i = 0}^\infty f(i)$ can be written as ∑' i, f i
The sum $\sum_{i = 0}^{n - 1} f(i)$ can be written as ∑ i in Finset.range n, f i

[Mitchell Lee]

You will need to prove yourself that every function to ℕ∞ is summable (docs#Summable), but you should not need to introduce your own notation or function for the sums.

[Peter Nelson]

I wrote some code for this that can be found in https://github.com/apnelson1/Matroid/blob/main/Matroid/ForMathlib/ENatTopology.lean.

The relevant API is roughly in lines 200-400. I think it should be PRed, but I haven't got around to it.