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.

[Lua Viana Reis]

@Oliver Butterley here is a quick proposal for a plan:

• update the repository to latest mathlib and lean
• write the lemmas in the *PR.lean files in their full generality, then create branches and PR them to mathlib
• discuss how to remove the measurability assumption of the observable in the main file and remove it
• create a branch and a PR for the main file

[Lua Viana Reis]

in the "create a branch" steps also adequate the code to match mathlib convention and style

[Oliver Butterley]

That sounds great! I ready to help with whatever task where you think I could be useful. Feel free to assign me tasks. I'm curious about the measurability issue but I suspect it doesn't make sense to discuss the details until everything is updated.

[Lua Viana Reis]

feel free to start with the first two points, I can talk here and merge PRs but I'll not be working on them the next days myself

[Oliver Butterley]

Lua Viana Reis said:

feel free to start with the first two points, I can talk here and merge PRs but I'll not be working on them the next days myself

OK, I'll do that.

[Oliver Butterley]

Updating the code from one year ago was hard work! Many things have been deprecated or modified since then. The git -S helped a lot to find the deprecations deep in the git history. :persevere:
I did a PR to the repo with the updated code. There are still 3 sorrys left but it had already taken hours to do all the other corrections required by the update so I didn't have time today for these.

[Lua Viana Reis]

thank you :) I fixed the sorries and merged

[Oliver Butterley]

I made a start of generalizing the partialSups lemmas.

It is work in progress but I opened a PR so you can see exactly how things stand and I won't be able to do more until tomorrow. I hope I didn't miss something obvious but it became rather involved because it seems some relatively standard results aren't available in full generality.

[Oliver Butterley]

Lua Viana Reis said:

thank you :) I fixed the sorries and merged

That's great!

[Oliver Butterley]

I believe all the lemmas in the *PR files are in reasonable generality now after my latest updates. @Lua Viana Reis let me know if there is something in those files that is still not the way it should be.

[Oliver Butterley]

Lua Viana Reis said:

Oliver Butterley here is a quick proposal for a plan:

• update the repository to latest mathlib and lean
• write the lemmas in the *PR.lean files in their full generality, then create branches and PR them to mathlib
• discuss how to remove the measurability assumption of the observable in the main file and remove it
• create a branch and a PR for the main file

@Lua Viana Reis I'm not a mathlib expert but I believe that now is a good time for creating branches of mathlib and preparing the PRs for things like the lemmas to add to BirkhoffSum, to BirkhoffAverage and to PatialSups. Moreover, arranged as PRs (even as drafts) it's much easier for others to give feedback and suggestions.

[Oliver Butterley]

Concerning the issue of removing the measurability assumption of the observable, I believe (as Sebastien wrote) that it is good to keep this as an assumption for most the lemmas and then argue at the end of the proof how this isn't actually required.

We should ask @Marco Lenci about this because I'm fairly sure he thought about this previously and understood how to do it. I think he also explained to me and then I forgot. Marco, would you be able to give a few comments about how the assumption can be dropped in the final part of the proof?

[Lua Viana Reis]

Isn't the argument just that if $\varphi$ is integrable and $f$ measure-preserving, then you can apply the current version with the completion of the sigma-algebra (NullMeasurableSpace) and then prove that the "ae" quantifier and both sides of the equation are still equal to the original? (better said than done, probably)

[Lua Viana Reis]

I will take a look at your PR today, in the last weeks I was working on making the infoview work in emacs (#lean4 > need help setting up lean4-infoview)

[Oliver Butterley]

Lua Viana Reis said:

in the last weeks I was working on making the infoview work in emacs (#lean4 > need help setting up lean4-infoview)

:rofl: the sort of unexpectedly huge technical task that I'm normally attracted to. Good luck with it! For lean vscode is very well supported and on this I'm lazy!

[Oliver Butterley]

Lua Viana Reis said:

Isn't the argument just that if $\varphi$ is integrable and $f$ measure-preserving, then you can apply the current version with the completion of the sigma-algebra (NullMeasurableSpace) and then prove that the "ae" quantifier and both sides of the equation are still equal to the original? (better said than done, probably)

That is completely convincing mathematically! Maybe it works nicely as a wlog in the last part.

[Marco Lenci]

Oliver Butterley said:

We should ask @Marco Lenci about this because I'm fairly sure he thought about this previously and understood how to do it. I think he also explained to me and then I forgot. Marco, would you be able to give a few comments about how the assumption can be dropped in the final part of the proof?

Hello both,
I'm confused as to why I've been summoned from Lean obscurity. :sweat_smile: If the issue is what formalization is preferable in terms of the hypothesis on the observable, I'm not sure I can help. (Even on the purely mathematical side, I never went into the fine details of differentiating between measurable and strongly measurable.)

What I mentioned to @Oliver Butterley once was that the Katok-Hasselblatt proof of the Birkhoff Ergodic Theorem is rather convenient for Lean too because, save for the last few lines, it provides the explicit invariant zero-measure set in the complement of which the Birkhoff average exists (this formulation is not 100% correct, but it should point you close enough to what I mean). That way, the complications due to the fact the the Birkhoff average only exists almost everywhere are dealt with in Lean with minimal effort.

[Oliver Butterley]

Lua Viana Reis said:

I will take a look at your PR today, in the last weeks I was working on making the infoview work in emacs (#lean4 > need help setting up lean4-infoview)

@Lua Viana Reis Were the generalised lemmas as you wanted? Any further changes I should make?

[Oliver Butterley]

In preparation for dropping the measurability assumption in the main theorem of BET I started on some of the required lemmas. #26074 includes the lemma that the birkhoffAverage of an integrable observable is equal to the birkhoffAverage of the measurable version of the observable (docs#MeasureTheory.AEStronglyMeasurable.mk).

[Oliver Butterley]

I added the argument which proves the measurability of the observable assumption to be dropped in the final statement.

[Oliver Butterley]

Lua Viana Reis said:

Oliver Butterley here is a quick proposal for a plan:

• update the repository to latest mathlib and lean
• write the lemmas in the *PR.lean files in their full generality, then create branches and PR them to mathlib
• discuss how to remove the measurability assumption of the observable in the main file and remove it
• create a branch and a PR for the main file

We are doing well on the plan! There are small improvements to be made to the main proof but it is a complete argument. It's time to PR some of the parts and proceed refining everything.

@Lua Viana Reis how would you like to proceed? Shall I start with doing the PRs to mathlib for the *PR.lean files?

[Lua Viana Reis]

Hi Oliver, that's a lot of progress, thanks! Sorry for the delay, I think I'll just merge your PR; you probably had more time to think it through than I have now. In any case I'll read it and post relevant comments there

[Lua Viana Reis]

Oliver Butterley said:

how would you like to proceed? Shall I start with doing the PRs to mathlib for the *PR.lean files?

If you prefer I can create them this afternoon

[Oliver Butterley]

Lua Viana Reis said:

Oliver Butterley said:

how would you like to proceed? Shall I start with doing the PRs to mathlib for the *PR.lean files?

If you prefer I can create them this afternoon

That would be great! My working day finished an hour ago so I won't do anything until tomorrow. If you leave me a message with instructions I can carry on the work when I wake up.

[Lua Viana Reis]

@topic are these small lemmas worth PRing to .Filter.Basic? They make this calc proof more readable by allowing dot notation

namespace Filter.EventuallyEq

variable {f : Filter α} {f₁ f₂ f₃ : α → β} [Mul β]

@[to_additive]
lemma mul_right (h : f₁ =ᶠ[f] f₂) : f₁ * f₃ =ᶠ[f] f₂ * f₃ := mul h (by rfl)

@[to_additive]
lemma mul_left (h : f₁ =ᶠ[f] f₂) : f₃ * f₁ =ᶠ[f] f₃ * f₂ := mul (by rfl) h

[Lua Viana Reis]

(most importantly, nested dot notation like h.add_right.neg.add_left to apply h to a term inside the expression --- perhaps there is some sort of conv that does this for filters?)

[Oliver Butterley]

My personal opinion is that mul_right and mul_left could be added to Mathlib.Order.Filter.Basic but I'm not a mathlib expert.

From a practical point of view I would suggest opening the small PR to mathlib which adds these two lemmas. As a PR it is much easier for experts to give feedback.

[Lua Viana Reis]

Is there any convention on the order in which theorems appear in a file? (my intuition was to group with related statements if possible)

And in the use of theorem vs lemma?

[Edward van de Meent]

it is my experience that lemma has the best ease of typing to rejection ratio

[Lua Viana Reis]

thing is, the whole (existing) file is just theorems and I think it gonna look akward to have my new statements be the only lemmas

[Ruben Van de Velde]

(All code translated from lean 3 used theorem.)

[Lua Viana Reis]

Ruben Van de Velde said:

(All code translated from lean 3 used theorem.)

Still, I think talking about it in the contributing guidelines would be good... I remember the instructions were very detailed for the mathport, so now the freedom makes me insecure

[Lua Viana Reis]

I'm of the opinion that in code, if there is a semantically meaningless difference, then better have no difference at all (so no lemma). I probably have to find the topic discussing why it was brought back

[Kevin Buzzard]

It seems that there is a big split of opinion here between those with a more CS background (who want an algorithm and are confused about the fact that there are two options) and mathematicians (who have just been solving this problem by vibes for centuries and can't see what the fuss is about)

[Lua Viana Reis]

I'm a mathematician :p and I do like writing lemmas, just not in software! :)

I think the nicest option would be an attribute like @[important], signaling that some theorem is one of the main things in the file

[Lua Viana Reis]

Since previous theorems were not turned into lemmas after mathport, the current situation looks like a big mess to me

[Kevin Buzzard]

I agree that the port was a setback to the whole vibes thing but we're doing our best to insert new vibes back into mathlib4 and will probably continue to do so until we're forcibly stopped

[Aaron Liu]

Does it even matter?

[Lua Viana Reis]

it does in the sense it is meant to convey some _meaning_, but this is not enforced (and currently, the use does not reflect the intended meaning)

[Lua Viana Reis]

if we used an attribute like @[important] or @[main_result], then this intended meaning could be used to automatically extract actual stuff like a "list of main results"

[Lua Viana Reis]

I was thinking recently, it would be very nice if we used more attributes to tag informal/cultural information for theorems in mathlib. We could have attributes like @[informal_name "Birkhoff Ergodic Theorem"] (or even a list of such informal names) that would be very very useful for docs and search tools

[Weiyi Wang]

Lua Viana Reis said:

or even a list of such informal names

The 1000+ theorem list occasionally served this purpose for me

[Weiyi Wang]

Also about lemma vs theorem, I would find it more useful if it is reflected in the doc. Currently it seems all lemma is displayed as theorem in the doc

[Lua Viana Reis]

@Weiyi Wang exactly! A list like that could easily be automatically generated if we tagged more information on the theorems, and the docs could reflect this information. I was also thinking about more editor tooling, e.g. "jump to theorem" where you can write the informal name

[Lua Viana Reis]

I think I'll put a proof-of-concept library for this in my todo list

[Michael Rothgang]

There's been lots of previous discussion on the lemma-vs-theorem issue. A few incremental improvements that are possible already are:

• if something should be a theorem, make sure it has a doc-string (this was one of the proposals from these threads, I don't think it's enforced yet)
• there's an informal preference that named theorems should have their name in bold (as in the **central limit theorem**; PRs adding this are welcome)
• I think the 1000+ theorems list could serve the purpose of a lookup table: making it more useful rests on making the table more complete. More specifically, help that does
  • add missing entries to the wikipedia list (see here for some inspiration)
  • ask very nicely so @Freek Wiedijk updates the list of theorems tracked by the project. (This is auto-generated by a script, so in principle very possible. Knowing "Wikipedia's list just got much better" could be a reason to spend the time on an update. Also tracked here on the 1000+ theorems repository)
  • help with filling in the Lean data for formalised theorems. My guess is that the current list is fairly complete; new entries to the list will change this, of course.

[Michael Rothgang]

All of this is incremental, so even small contributions in the right direction can be helpful.

[Michael Rothgang]

Oh, and I forgot: convince people in the Isabelle/Rocq/Metamath community that this list is cool, so they should be adding data about their formalisations :-)

[Oliver Butterley]

Michael Rothgang said:

- add missing entries to the wikipedia list (see [here] for some inspiration)

Where? Which wikipedia list?

[Ruben Van de Velde]

https://en.wikipedia.org/wiki/List_of_theorems ?

[Michael Rothgang]

The list of missing items is https://github.com/1000-plus/1000-plus.github.io/issues/32. Sorry for sending this too early.

[Oliver Butterley]

Lua Viana Reis said:

Oliver Butterley said:

how would you like to proceed? Shall I start with doing the PRs to mathlib for the *PR.lean files?

If you prefer I can create them this afternoon

Hi @Lua Viana Reis, I got distracted away from the main purpose here. Are there some more things I can help with in the process of PRing your proof of Birkhoff's ergodic thm? My impression is that:

• There are many small lemmas in the separate files which which are in a good state and need to have mathlib PRs done.
• Then there is the main file of the proof which is mostly in a good condition. I think there could be some tidying of the file, renaming of the statements, complete doc string for the main statement, etc. Possibly also the use of ℝ in {φ : α → ℝ} can be slightly generalised.
  Give me instructions if there is something I can do.

[Lua Viana Reis]

Hi @Oliver Butterley, yes, I've been juggling a few different things in life and was not able to allocate time to the birkhoff PR. I'm without a fixed source of income and not yet sure where I'll do my PhD, so this situation may continue in the next months. I've also forbidden myself from working on the computer at night like I used to do, for health-related reasons. But please note that it's all open sourced, so there is no problem if you want to do it yourself :)

[Oliver Butterley]

I'm sorry for you, that's not a very comfortable position to be in. I hope you find a great solution soon! Very wise to reduce night time use of computers, I learnt this only a short time ago. :healthier: :happy:

I would happily support your application for a PhD at my university but, given your interests and skills, I suspect another university would be a far better choice for you. Let me know if I can help with anything connected to this. Good luck with it all!

[Oliver Butterley]

You did a great work with the proof of Birkhoff's ET. I'll proceed with doing the PRs and any final tidying. I'm doing some other stuff which builds on BET so it will be convenient to have BET finalized.

[Oliver Butterley]

I prepared the PR for the main theorem: #26923 and multiple PRs for all the little lemmas that belong somewhere else in mathlib. The changes I made compared to your version @Lua Viana Reis were mostly things to match mathlib style, e.g., replacing cases', etc.

[Oliver Butterley]

Conversation continues in the PR reviews channels: #PR reviews > #26923 The pointwise ergodic theorem (Birkhoff's)