Birkhoff Ergodic Theorem

Stream: mathlib4

[Lua Viana Reis]

I'm creating this topic to discuss a possible PR of the proof of pointwise Birkhoff to mathlib. The complete proof I have can be found here. Under the library folder, there are three files with some results that I think should go into other existing files in mathlib. I have not contributed to mathlib before other than during the mathport, so some help is very appreciated :)

Some relevant comments:

• Should everything in the main file stay in a single file? It feels like the bit about the sigma algebra of invariant sets could live in another file;
• Docstrings are missing;
• The results in BirkhoffSumPR are specialized to $\mathbb{R}$ because I had a hard time figuring out the most general type classes while also keeping the simp + linarith proofs;
• On this line I need to assume $\varphi$ is integrable and measurable. It seems like being AEStronglyMeasurable is not enough but perhaps it is;
• Not sure to which file this basic lemma should go;
• Is this lemma about a sigma-algebra being a subset of its null set completion really missing? I could not find it

@Sébastien Gouëzel @Pietro Monticone

[Kim Morrison]

Anytime you think something could go in a separate file, you are probably right. :-) Also, this will need to be multiple PRs, and do this "file at a time" is often a good approach.

[Sébastien Gouëzel]

A few comments:

• More files is almost always better. So I think the definition of the invariant sigma algebra should definitely go into its own file. But note that this is already in Mathlib, in docs#MeasurableSpace.invariants (with a small API around it).
• The most efficient way is indeed to PR one file at a time, because it's much easier for reviewers (and also you will learn some tricks along the process, so later PRs will be smoother).
• Indeed, typeclasses will need to be generalized in BirkhoffSumPR. linarith shouldn't be relevant -- the assumptions should essentially be the same as in the definition of Birkhoff averages.
• Integrability of the function should indeed be enough, you shouldn't need to assume measurability in addition. However, if it is more convenient for some auxiliary lemmas, you can definitely prove them with the additional assumption, and then drop it in the final version of the interesting results by reducing to the measurable case.
• The basic lemma you mentions already exists, as docs#abs_le_max_abs_abs (I found it just by doing by exact? on your lemma).

[Lua Viana Reis]

• The basic lemma you mentions already exists

Oh, I did try exact? first but it failed since it was stated with ⊔ instead of max.

[Lua Viana Reis]

linarith shouldn't be relevant

Yes, I was just lazy at the time to find the proofs without it.

[Lua Viana Reis]

Hi all! sorry for the hiatus. I went to my family home to do a small dental surgery and then to Italy. The ICTP school is over so I can have more time for it now.

[Lua Viana Reis]

The proof is now using docs#MeasurableSpace.invariants, I'm now working in dropping the stricter measurability assumption. It seems the easiest way is to drop it in the final version of the theorem, because some theorem related to restriction of measures requires strict measurability of some sets. Before travelling I attempted to drop the assumption everywhere and got stuck. I can't remember which one it was right now and I'm still away from the desktop computer in which the attempt was made.