Summer project: dynamics and ergodic theory

Stream: new members

[Lior Silberman]

One of my summer students is interested in formalizing further definitions and theorems in dynamics and ergodic theory not yet in mathlib (it would be nice to reach the Birkhoff Ergodic Theorem, for example).

Is this reasonable? How do I tell if someone else is working on this?

[Yury G. Kudryashov]

It is on my todo list but I would love to see it done by someone else. I'll write more details tomorrow.

[Anatole Dedecker]

I am also interested in seeing more dynamics in Mathlib, but I haven’t really interacted with this at all yet so Yury will be more helpful.

[Yoh Tanimoto]

I think @Marcello Seri @Oliver Butterley @Marco Lenci are doing exactly the Birkhoff Ergodic theorem

[Lior Silberman]

Let's see what they say then. We can work toward other goals, e.g. entropy or topological dynamics.

[Oliver Butterley]

Thanks Yoh for connecting us.

Marcello and Marco started a while ago under the guidance of Sebastien Gouezel in a Lean workshop. I joined them more recently. Progress to date is in this repo. We have some bursts of progress and then there are long periods of time when we have too many other commitments to devote time to it.

Personally I have no interest in being possessive of this or anything else. I'm just keen to use what energy and time I have spare in order to add a bit. Extending the dynamics content is my focus. We should coordinate!

[Patrick Massot]

@Damien Thomine also worked on topological entropy but I don’t know the current status of this project.

[Lior Silberman]

I just don't want to duplicate effort, so let's coordinate. For now I'm getting the student going.

By the way, in which part of the form do I post technical questions/discussions?

[Lior Silberman]

@Yoh Tanimoto thanks!

[Yury G. Kudryashov]

Note that we have docs#ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection

[Yury G. Kudryashov]

BTW, I suggest that you start contributing parts of your project to Mathlib early, so that it doesn't rot before it gets merged.

[Marcello Seri]

It would be nice if your student wants to join our effort, is quite well on the way and while indeed we can commit to it only at certain times, the ci is checking periodically compatibility and (at least I) can commit to review PRs

[Pietro Monticone]

@Lorenzo Luccioli and I have just opened a PR golfing a few proofs in Topological.lean and fixing a few typos in Birkhoff.lean.

[Marcello Seri]

Thanks

[Marcello Seri]

We keep some more work on branches, like https://github.com/mseri/BET/tree/wip

[Yury G. Kudryashov]

Another reminder to start opening mathlib PRs with helper lemmas from your project. Even if the project is not ready yet, you probably have quite a few useful helper lemmas.

[Oliver Butterley]

Yep, keeping the code tidy and promptly opening mathlib PRs with any useful parts is a sensible plan. But my son is a few months old, this semester I had to prepare and teach a new course, etc and so sensible plans don't always get implemented! :rofl:

Concerning topological dynamics, I later noticed that some of what we looked at is already in mathlib but there are a few bits that we had done which could be added. @Pietro Monticone and @Lorenzo Luccioli , maybe we could could chat about this and get this done?

However there is a huge amount of topological dynamics which is currently not in mathlib! No shortage of things to do for everyone who wants!

As Yury mentioned, the mean ergodic theorem is in mathlib. The most advanced version we have of the pointwise ergodic theorem (birkhoff) is in our wip branch.

[Yury G. Kudryashov]

Congratulations about the son!

[Pietro Monticone]

We have almost finished golfing all the proofs in Topolical.lean.

In this example we don't really understand why we get the following linter warning:

unused variable `h`
note: this linter can be disabled with `set_option linter.unusedVariables false`

We've reproduced the same warning with the following MWE:

example (Q : Prop) (q : Q) (h : ¬ Q) : Q := by
  contrapose! h
  exact q

Can anybody explain, please?

[Ruben Van de Velde]

Well, you're not using the h

[Yoh Tanimoto]

in the sense that you can remove both (h : ¬ Q) and contrapose! hfrom the proof and it is still a correct proof

[Pietro Monticone]

Yes, sorry. The MWE was probably too simple compared to the real case.

The point is that we're not sure how to avoid using minimality as the argument of the contrapose! in the original example below. It's true that minimality is not used after the contrapose!, but we have to specify it in order to contrapose it. Maybe there's some alternative tactic we may adopt, but we don't know any in this case.

/-- An example of a continuous dynamics on a compact space in which the recurrent set is all
the space, but the dynamics is not minimal -/
example : ¬IsMinimal (id : unitInterval → unitInterval) := by
  intro H
  have minimality := H.minimal
  contrapose! minimality
  -- `push_neg` pushes negations as deep as possible into the conclusion of a hypothesis
  use 0, 1, (mem_univ 0), (mem_univ 1), (dist (1 : unitInterval) (0 : unitInterval))/2
  -- we need this helper twice below
  have dist_pos : 0 < dist (1 : unitInterval) 0 := by
    apply dist_pos.mpr
    apply unitInterval.coe_ne_zero.mp; norm_num -- 1 ≠ 0
  constructor
  . apply div_pos dist_pos
    linarith -- 0 < 2
  . intro n
    -- `simp` is necessary to go from `¬id^[n] 1 ∈ ball 0 (dist 1 0 / 2)`
    -- to `0 ≤ dist 1 0`
    simp
    exact le_of_lt dist_pos

[Lior Silberman]

We'll download your code and read it. My goal would have been the pointwise ergodic theorem for L^1 functions on probability-preserving spaces. If that's done the next goal would be measure-theoretic and topological entropy and maybe the variational theorem.

[Pietro Monticone]

Draft turned into PR.

[Yoh Tanimoto]

maybe you can add the definitions of IsMinimal and H.minimal?

[Pietro Monticone]

Yoh Tanimoto said:

maybe you can add the definitions of IsMinimal and H.minimal?

Sure:

/-- A dynamical system (α,f) is minimal if α is a minimal subset. -/
def IsMinimal (f : α → α) : Prop := IsMinimalSubset f univ

and

/-- The minimal subsets are the closed invariant subsets in which all orbits are dense. -/
structure IsMinimalSubset (f : α → α) (U : Set α) : Prop :=
  (closed : IsClosed U)
  (invariant : IsInvariant (fun n x ↦ f^[n] x) U)
  (minimal : ∀ (x y : α) (_ : x ∈ U) (_ : y ∈ U) (ε : ℝ), ε > 0 → ∃ n : ℕ, f^[n] y ∈ ball x ε)

[Lior Silberman]

For invariance isn't the right definition that if x\in U then f(x)\in U? This implies that all powers of f have the same property, so the two definitions are equivalent, and in that case why make ourselves check the stronger condition.

[Lior Silberman]

Instead maybe make the equivalence a lemma

[Damien Thomine]

Thanks Patrick for paging me. First a few comments :

• I didn't write anything about measured dynamics (so no interference with the project on Birkhoff's theorem)
• I had written a few things about general topological dynamics, but it was just bits and pieces, and in Lean3. Most of it I did not port it to Lean4, and do not intend to. I would still have some advice if you're interested.
• The only part I did port was on invariant subsets. I'll put it on BET ASAP so that there is no duplicate work.
• I have a current project about topological entropy à la Bowen. It's pretty advanced, so better not to go in this direction.

[Damien Thomine]

For general topological dynamics: a reference I found quite useful is

Topological and symbolic dynamics - Petr Kurka

Frames everything in terms of relations on X x X, which is a very clean way to work.

[Damien Thomine]

@Lior Silberman : agree on the definition of invariance. The cleanest I found is $$U \sub f ^{-1}' U$$. No need to introduce points. In addition, the tactic simp tends to write subsets in normal form with preimages when possible; if you do the same, that means that simp works for you instead of against you. And it can be very annoying to work against simp.

[Damien Thomine]

@Marcello Seri @Oliver Butterley My current work on topological entropy is getting a bit extensive. Would it be possible to put it on BET so that we can exchange on it before putting it on MathLib? I've already got some more-or-less finalized stuff, but some review / external advice would be very welcome.

[Damien Thomine]

Finally, the current state of my work on topological entropy is :

• Definition of topological entropy à la Bowen using covers : done.
• Definition of topological entropy à la Bowen using nets : done.
• Equivalence of the two definitions : done.
• Behaviour of entropy for common systems (subsystems, unions, products, conjugacies...) : in progress.
• Entropy of a full shift : would be the next step.

Many non-obvious design decisions, which means some significant additional work on other structures.

[Oliver Butterley]

Hello, @Damien Thomine! It's been way too long since we have met in person! I hope all's well with you.

Concerning minimal sets, etc. I realised fairly recently that there is some stuff in Dynamics/Minimal and so we should try to match with that and no duplicate. I have some extra pieces, for existence the proof of the existence of minimal sets using Zorn's lemma, etc but I still have them in a branch of a fork of BET.

I know, this is ridiculous of me, I should have merged everything properly a few months ago so that it was easier for everyone to see what is what. However that was just the moment my partner returned to work after maternity leave and our son didn't start in the nursery until a few months later. So I had a few months of playing, not sleeping and failing to do sensible organization of code!

@Pietro Monticone and @Lorenzo Luccioli, you guys are efficient! Sorry if my lack of organization at the moment has been an inconvenience. Let me figure out a way to put all of your stuff together. But then we probably need to find what we need to modify to fit with what's already in mathlib.

I like Damien's suggestion, we can keep the repo as more or less good and complete, in preparation for moving to mathlib but be a bit more relaxed about our standards. From this week onwards I finally have time to work again and I'm happy to use time on this.

[Pietro Monticone]

Don’t worry, Oliver. No problem at all for us!

[Yoh Tanimoto]

Pietro Monticone
I don't know what to do with this ¬ of a structured Prop, but can you do something like this?

def IsMinimalSubset (f : α → α) (U : Set α) : Prop :=
  (IsClosed U) ∧ (IsInvariant (fun n x ↦ f^[n] x) U) ∧ (∀ (x y : α) (_ : x ∈ U) (_ : y ∈ U) (ε : ℝ), ε > 0 → ∃ n : ℕ, f^[n] y ∈ ball x ε)

example : ¬ (IsMinimalSubset (id : α → α) univ) := by
  rw [IsMinimalSubset]
  push_neg
  sorry

[Yury G. Kudryashov]

See also @[mk_iff]

[Yoh Tanimoto]

maybe there is a shorter code but I think this way you can avoid minimality

import Mathlib

variable (P Q : Prop)

structure S : Prop :=
  (sP : P)
  (sQ : Q)

example : ¬ (S P Q) := by
  by_contra!
  rw [← and_not_self_iff Q]
  apply And.intro this.sQ _
  sorry --need to prove ¬ Q

[Pietro Monticone]

Thank you everyone for your suggestions!

We have just solved the "unused variable minimality" problem as follows:

/-- An example of a continuous dynamics on a compact space in which the recurrent set is all
the space, but the dynamics is not minimal -/
example : ¬IsMinimal (id : unitInterval → unitInterval) := by
  intro H
  have minimality := H.minimal 0 1 (mem_univ 0) (mem_univ 1)
    ((dist (1 : unitInterval) (0 : unitInterval)) / 2)
  revert minimality; contrapose!; intro _
  -- we need this helper twice below
  have dist_pos : 0 < dist (1 : unitInterval) 0 :=
    dist_pos.mpr (unitInterval.coe_ne_zero.mp (by norm_num))
  refine' ⟨div_pos dist_pos (by norm_num), fun n ↦ _⟩
  -- `simp` is necessary to go from `¬id^[n] 1 ∈ ball 0 (dist 1 0 / 2)`
  -- to `0 ≤ dist 1 0`
  simp only [iterate_id, id_eq, mem_ball, not_lt, half_le_self_iff]
  exact le_of_lt dist_pos

Pushed in the same PR.

[Oliver Butterley]

@Lorenzo Luccioli @Pietro Monticone Thanks again for the PR.

Did you think more about the minimal set stuff when you were going through it? Now all the minimal stuff is isolated into a separate file and in another PR some extra things about existence and different equivalent definitions added.

[Oliver Butterley]

Damien Thomine said:

For general topological dynamics: a reference I found quite useful is

Topological and symbolic dynamics - Petr Kurka

Frames everything in terms of relations on X x X, which is a very clean way to work.

Thanks for the reference suggestion. I didn't previously have a favourite for these topics and I like that the electronic version is freely downloadable.

[Pietro Monticone]

Oliver Butterley said:

Lorenzo Luccioli Pietro Monticone Thanks again for the PR.

Did you think more about the minimal set stuff when you were going through it? Now all the minimal stuff is isolated into a separate file and in another PR some extra things about existence and different equivalent definitions added.

Hi Oliver, you're welcome. We'll take a look at the new content in the next few days paying closer attention to Minimal.lean.

[Oliver Butterley]

Oliver Butterley said:

Thanks for the reference suggestion. I didn't previously have a favourite for these topics and I like that the electronic version is freely downloadable.

Although the content related to minimal sets in that book is overly minimal : :joking:

[Oliver Butterley]

Pietro Monticone said:

Hi Oliver, you're welcome. We'll take a look at the new content in the next few days paying closer attention to Minimal.lean.

Would it be useful to chat about it sometime?

It appears there are a few "design" decision to make on this topic which aren't immediately clear. How about, we both take a look both at what we have and what exists in mathlib already (linked in our file), then we can have a chat an hopefully see a clear route to proceed?

[Pietro Monticone]

Oliver Butterley said:

Would it be useful to chat about it sometime?

It appears there are a few "design" decision to make on this topic which aren't immediately clear. How about, we both take a look both at what we have and what exists in mathlib already (linked in our file), then we can have a chat an hopefully see a clear route to proceed?

We're both going to be quite busy in the following weeks (we can probably find the time to simplify some proofs, but not much more)... How about taking a look at all this in Pisa next month?

[Oliver Butterley]

Great! Let's discuss when we see each other in Pisa. Looking forward to it!

[Pietro Monticone]

We have just opened a PR golfing a few proofs in Minimal.lean.

[Lua Viana Reis]

Hi all, I've a sorry-free version (except for a silly lemma) of the same statements in Birkhoff.lean of @Marcello Seri's repo. This is a different file because I already had some lemmas from an attempt I had at proving Birkhoff some months ago, and the approach is a bit more succinct. This week I bought myself a fast computer so I'm motivated to write more things in Lean (it was not quite a good experience in the laptop). I'm planning to finish the proof this weekend if possible.

https://github.com/lucasvreis/BirkhoffErgodicThm/blob/main/BirkhoffErgodicThm.lean

[Lua Viana Reis]

In case anyone wants to golf the silly lemma:

lemma abs_le_bound (a b c : ℝ) : (a ≤ b ∧ b ≤ c) → abs b ≤ (abs a ⊔ abs c) := sorry

[Mitchell Lee]

lemma abs_le_bound (a b c : ℝ) (h1 : a ≤ b) (h2 : b ≤ c) : |b| ≤ |a| ⊔ |c| := by
  simp_rw [abs_eq_max_neg, max_le_iff]
  aesop

[Luigi Massacci]

Lucas Viana Reis said:

This week I bought myself a fast computer so I'm motivated to write more things in Lean (it was not quite a good experience in the laptop). I'm planning to finish the proof this weekend if possible.

I guess it doesn't concern you anymore, but just so you know you can use Lean on gitpod for free, and the large workspace works pretty well, and since you are working on free software you can ask them to up you to 250h/month of free time (default is 50)

[Lua Viana Reis]

Mitchell Lee said:

lemma abs_le_bound (a b c : ℝ) (h1 : a ≤ b) (h2 : b ≤ c) : |b| ≤ |a| ⊔ |c| := by
  simp_rw [abs_eq_max_neg, max_le_iff]
  aesop

Cool! I had forgotten about aesop

[Lua Viana Reis]

This is nice to know, but for 50 hours they are asking for a LinkedIn acount :sweat_smile:

[Yaël Dillies]

Really? They didn't back when I started using it

[Kevin Buzzard]

Probably people figured out how to mine bitcoin using it or something

[Lua Viana Reis]

image.png

Actually they show you this, but if you "continue with 10h" then you also get 50 :shrug:

[Lua Viana Reis]

Lucas Viana Reis said:

Hi all, I've a sorry-free version (except for a silly lemma) of the same statements in Birkhoff.lean of Marcello Seri's repo. This is a different file because I already had some lemmas from an attempt I had at proving Birkhoff some months ago, and the approach is a bit more succinct. This week I bought myself a fast computer so I'm motivated to write more things in Lean (it was not quite a good experience in the laptop). I'm planning to finish the proof this weekend if possible.

https://github.com/lucasvreis/BirkhoffErgodicThm/blob/main/BirkhoffErgodicThm.lean

There is now 1 "straightforward" sorry left in the main proof and three in BirkhoffSumPR that should help with the first sorry (show that the birkhoff average of sum of functions is the sum of averages, and also for neg). I may only touch it next weekend, but if anyone wants to complete those and PR it please feel welcome.

[Lua Viana Reis]

Also the proof is probably miles away from being mathlib-ready, contributions in this direction are also very welcome

[Lua Viana Reis]

I couldn't resist and made it sorry free, at the expense of specializing the auxiliary lemmas to \R :smile:

[Lua Viana Reis]

(deleted)

[Lua Viana Reis]

image.png

[Lior Silberman]

Since the ergodic theorem is already well in hand, we'll work on metric (Kolmogorov--Sinai) entropy.

[Lua Viana Reis]

There are also a lot of things related to Birkhoff that I think would be nice to have, like the maximal ergodic theorem, the corollary for continuous functions on metric spaces and even the ergodic decomposition and Kingman's.

[Lior Silberman]

I assume the maximal ergodic theorem is a stage in the proof of the pointwise theorem?

[Sébastien Gouëzel]

The most efficient proofs of the pointwise theorem (such as the one in Katok-Hasselblatt) go through a maximal argument, but less precise (and easier) than the maximal ergodic theorem.

[Lua Viana Reis]

I was following the proof in "Conformal Fractals" from Przytycki and Urbański, it only uses a very special case of the maximal theorem.

[Lua Viana Reis]

I'm also not claiming the proof that has been written is the one that should go to mathlib, it was mostly a weekend project for me (but afaik, previous formalizations also used this shorter proof). I think it would be nicer to have it either as a corollary of Kingman's or as a corollary of the maximal theorem and Banach principle, since in the end we would have more useful statements.

[Lua Viana Reis]

By Banach principle, I mean the Birkhoff proof in here:
https://joelshapiro.org/Pubvit/Downloads/joel_aeconv_howto.pdf

The advantage is that this sort of result is also useful for many other things.

[Lior Silberman]

The notion we need here is weak L^p spaces.

[Sébastien Gouëzel]

We shouldn't have it as a consequence of Kingman, because most proofs of Kingman use Birkhoff :-)

[Lua Viana Reis]

In Krerley and Viana's book they have a somewhat combinatorial proof of Kingman without Birkhoff (originally by Avila I think)

[Lua Viana Reis]

and I think it's about the same length as a proof of Birkhoff using the maximal theorem

[Lua Viana Reis]

https://www.cmat.edu.uy/~lessa/tesis/Avila.pdf

[Lua Viana Reis]

(deleted)

[Sébastien Gouëzel]

If I remember correctly, the proof by Avila-Bochi has essentially the same flavor as a classical proof of Kingman due to Steele, but Steele's proof is quite simpler because it uses Birkhoff to discard the case where you have to wait too long before reaching the limit. Steele's proof (less than 2 pages) is here: http://www.numdam.org/item/AIHPB_1989__25_1_93_0.pdf.

[Sébastien Gouëzel]

@Lucas Viana Reis , it looks like your proof of Birkhoff is essentially ready (I mean, it looks both complete and clean!). Are you planning to PR it to Mathlib? It would be amazing to have Birkhoff in Mathlib.

[Sébastien Gouëzel]

If you need help on the process to contribute, just tell it here, I'm sure many people would be most happy to help you.

[Lua Viana Reis]

Thanks for the kind words @Sébastien Gouëzel :)
I'm willing to do it, but I never contributed to mathlib (other than the mathport) so I would have to learn how the process works. I think I will have some spare time in the beginning of July to create a topic in the #mathlib4 channel for this. I'm also preparing for my first international travel, I'll be at the ICTP school in Trieste this summer.

[Sébastien Gouëzel]

Great, just tell us when you need help. And ICTP is a great place (it was also my first international conference, 25 years ago :-)

[Oliver Butterley]

Hi @Lua Viana Reis, I see you have your complete proof of Birkhoff's ergodic theorem in your repo but you never opened a PR for adding it to mathlib. Can I help in anyway with the process?