Infinite sums and documentation

Stream: new members

[Philippe Duchon]

I am still trying to understand what Mathlib knows about infinite sums (other than "generally speaking, more than I do"), and when browsing the documentation on github, I notice that sometimes the documentation leaves things out that make it hard to understand what is going on.

An example is Summable.summable_compl_iff in Mathlib/Topology/Algebra/InfinteSum/Group.lean, which (as I understand by looking at the source code) says that if a sub-family is summable, then the complement sub-family is summable if and only if the full family is. But, when looking on github, the hypothesis appears as hf: Summable (f o Subtype.val), and the same appears in the equivalence statement, leaving out _which_ subtype one is talking about. The name makes it somehow clearer, but I still find this confusing.

Is this some secondary effect of the way the documentation is extracted from the source code? The statement in the source contains type annotation which are lost in the extracted documentation, and which make the meaning much clearer.

Of course in this case I was looking for the right statement and the name helped me find it, but it seems likely that there will be other, similar cases, that are not that obvious.

Also, on a slightly different matter, but still about infinite sums: Mathlib/Topology/Algebra/InfiniteSum/Real.lean has a lemma summable_partition that deals with the summability of an infinite family when it is arbitrarily partitioned - but only when the values are reals. Is there a good reason for this restriction? (I might very well be missing conditions that are required, but would something similar not hold in significantly more general situations?)

[Ruben Van de Velde]

docs#Summable.summable_compl_iff

[Ruben Van de Velde]

So I think what you're asking about is that in the source we have those expressions (f ∘ (↑) : s → α) and (f ∘ (↑) : ↑sᶜ → α) with explicit type annotation and those get lost in the rendered code in the documentation. What's going on here is that the documentation tooling parses the lean code, and then writes out some code from the parsed representation (this is called "pretty printing"), but this process can unfortunately lose information. We don't yet have code that will present the parsed representation into code that is guaranteed to be equivalent to the code you had in the first place. This is a known but hard problem

[Eric Wieser]

If you want to know what the code actually means, your best bet is to write #check the_theorem_name in a live lean session, and then click around the result

[David Loeffler]

The reason docs#summable_partition is stated for series of non-negative reals is because it's false otherwise. Let α = β = ℕ, let s n be the finite set {2 * n, 2 * n + 1} and let f n = (-1) ^n. Then f is not summable, but the expression on the RHS is. So it needs the order assumption that 0 ≤ f; that means it has to be stated in a complete linearly ordered space, and there aren't very many of those.

[Philippe Duchon]

Oh yeah, I missed the fact that the partition was quantified outside of the equivalence. So it was not, in fact, the lemma I was looking for - I was looking for one that would let me arbitrarily partition a summable family (and only looking for an implication, really, where summable f would be the assumption).