Splitting an infinite sum into an infinite sum of sums

Stream: new members

[Philippe Duchon]

Does Mathlib have theorems to split an infinite sum into an infinite sum of (possibly infinite) sums?

The only thing I have found is summable_partition, which is only for sums of nonnegative reals, is written as an equivalence, and says nothing about the value of the sum. What I was looking for was a theorem where global summability is an assumption, letting me replace the tsum with the tsum of tsums.

[Kenny Lau]

sounds like the dominated convergence theorem

[Kenny Lau]

I think that's Summable.tsum_prod_uncurry:

∑' (p : β × γ), Function.uncurry f p = ∑' (b : β) (c : γ), f b c

[Philippe Duchon]

This requires a product, which will be uneasy to setup if some of the sub-sums have only a finite range (which happens to be true in the use case I have in mind).

This could become a new goal for my learn-by-doing formalisation project (which keeps changing every few weeks), but I'm really unfamiliar with the level of generality that Mathlib uses for topology.

[Kenny Lau]

@Philippe Duchon part of the art of asking a good question is asking a good question :upside_down:

In this case instead of the independent "product", you want a dependent "sigma type", and in that case it is Summable.tsum_sigma:

∑' (p : (b : β) × γ b), f p = ∑' (b : β) (c : γ b), f ⟨b, c⟩

[Philippe Duchon]

Thanks! I went through the more obvious files of the library, but failed to check this one.

Looks like what I was looking for was HasSum.prod_fiberwise - or at least it should be close enough.

[Kenny Lau]

@Philippe Duchon there's a better way than looking into 100 files, if you know you want "tsum" over a "sigma" type, then you just write tsum, "sigma" in Loogle, and bob's your uncle

[Philippe Duchon]

That's a good idea, but I wasn't aware that what I wanted was to mix tsum and sigma types. I was thinking of "partition", but that did not find me much of interest.

This is, more generally, one of the difficulties I have with getting into Mathlib: if there are documents that explain, field by field, how the library is organized and how one should look for things in it, I have not found them so far. MIL does a great job of explaining parts of what I have in mind, but for very specific topics. So I do spend a lot of time browsing through files that look like they could contain what I want, but that is not very efficient. As a result, I tend to ask a lot of questions that turn out to be silly when you know where to look...

[Kevin Buzzard]

Asking lots of questions is fine. In the Imperial course we try and prove basic results in many areas to introduce students to each area but it's still not enough if you're going deeper into one area

[Kenny Lau]

Philippe Duchon said:

if there are documents that explain, field by field, how the library is organized and how one should look for things in it

that sounds like a task for LLM (AI)

[Ruben Van de Velde]

It very much doesn't

[Yaël Dillies]

MIL aims to do some of this