existence of local flows

Stream: mathlib4

[Winston Yin (尹維晨)]

I've formalised the existence theorem for local flows of vector fields by refactoring Analysis/ODE/PicardLindelof (#20704). I have also formalised the lemma that the solution is Lipschitz continuous in the initial condition (#20733), and the lemma that $C^n$ vector fields have $C^n$ solutions, but I would like to hear some feedback on the refactor first, before submitting more PRs. I'm pinging @Yury G. Kudryashov who authored the original file and @Michael Rothgang who expressed interest in reviewing it.

Things I learnt (which are probably obvious to others):

1. The best way to understand all the design choices of a formalisation is to do it from scratch yourself. I rewrote my own formalisation multiple times over several days, with moments of "aha, that's why Yury wrote it that way", until I felt comfortable going beyond the choices Yury had made.
2. It is incredible how big a gap in rigour there is between a maths textbook and the formalisation. The process of formalisation forced me to stare at the same obvious proof for days, which exposed many errors in the textbook.
3. The tooling can still be improved. For example, Lean makes manipulating integrals (on the real line) much more tedious by asking for integrability all the time, when normally you already know the function is integrable by virtue of having written an integral of it earlier. There is also a lack of tactics for intervals (t ∈ Ioo (t - ε) (t + ε), etc.) and min/max (|b - d| ≤ max (c - d) (d - a) whenever a ≤ b ≤ c), even though they're often just glorified inequalities needing some case analysis. I'm hoping something can be built for this.
4. Good type-theoretic design is very important. Because I did not have the foresight, I had to rewrite the definition of a structure many times to suit use cases as they come up, either for mathematical generality or type theory limitations (avoid propositional equality of types!).

[Yury G. Kudryashov]

Sounds very good. Unfortunately, I won't be able to review it until next week (I'm traveling, and I forgot my personal laptop).

[Patrick Massot]

It sounds like the whole story of ODEs in Mathlib could make a nice formalization paper. I think you should consider https://icetcs.github.io/frocos-itp-tableaux25/itp/

[Winston Yin (尹維晨)]

#21286 shows that solutions to $C^n$ ODEs are themselves $C^n$ in time, and #21777 (WIP but sorry-free) shows the existence of local flows on manifolds.

Couple directions to go from here. We now have all the ingredients to show that $C^1$ vector fields on compact manifolds define global flows on the manifold. I would also like to formalise the theorem that $C^n$ vector fields have $C^n$ dependence on the initial condition, following Lang's Fundamentals of Differential Geometry (pp. 81-88), but this is currently waiting for a corollary of the implicit function theorem. This proof is the longer of two proofs given in the book, but it can be generalised to $H^n$ spaces.

On the Lie group side, a little over a year ago, I wanted to formalise that left-invariant vector fields on Lie groups define global integral curves, but at the time, mathlib was missing:

• Lie groups are manifolds without boundary
• Lie groups are Hausdorff (T2Space)
• Left-invariant vector fields are smooth
  which have possibly been added to mathlib since then(?)

[Sébastien Gouëzel]

The fact that left-invariant vector fields are smooth is proved in #18396 (constructing the Lie algebra of a Lie group in full generality), but this is not merged yet. For the fact that Lie groups are manifolds without boundary, I think we need invariance of domain, so don't hold your breath (but you could just assume it as a typeclass assumption, with a todo saying to remove it).

[Sébastien Gouëzel]

I forgot to answer your question about the fact that Lie groups are T2. This is essentially already in mathlib (albeit not an instance, as Lean would have no way to guess the model space): it follows from the fact that charted spaces are T1 (docs#ChartedSpace.t1Space) and that a T1 topological group is T2 (found by infer_instance, the key point is docs#TopologicalGroup.regularSpace)