Riemannian manifolds

Stream: PR reviews

[Sébastien Gouëzel]

I have a big work in progress towards Riemannian manifolds in #25347. It will need quite a long string of PRs to get there. I will list the currently opened PRs here as a subtle hint :-) Currently, there are two kind of prerequisites, the ones on differential geometry, and another bunch towards a good change of variables formula in dimension 1 for monotone maps (to be able to talk about path length and reparameterize the paths nicely).

[Sébastien Gouëzel]

#25383 (+273/-29): continuity statements for the bundle of continuous linear maps

[Sébastien Gouëzel]

#25768 (+33/-2): derivative of continuous affine maps

[Sébastien Gouëzel]

#25771 (+32/-12): drop an assumption in congruence lemma for manifold derivatives

[Sébastien Gouëzel]

#25824 (+164/-63): require that the range of a real or complex model with corners is convex

[Sébastien Gouëzel]

#25865 (+420/-138, but completely mechanical and boring): add fun_ variants for Fréchet derivative of addition and like

[Sébastien Gouëzel]

#26066 (+70/-3): missing API for measure theory

[Sébastien Gouëzel]

#26068 (+135/-3): the derivative of a monotone function is nonnegative

[Sébastien Gouëzel]

#26069 (+114/-66): split the file MeasureTheory.Function.Jacobian

[Sébastien Gouëzel]

(And yes, I'm aware that's a long list!)

[Kevin Buzzard]

I'm only seeing this 12 hours later and it looks like a very short list now :-)

[Michael Rothgang]

I'm assuming we'll get some more PRs tomorrow/soon :-)

[Sébastien Gouëzel]

The reviewers have been incredibly efficient on the list of PRs above, thanks a lot of that. Let's add a few more PRs to the list, and see if things go as smoothly :-)

[Sébastien Gouëzel]

#26112 (+173/-19): applying a smooth hom bundle section to a smooth section gives a smooth section

[Sébastien Gouëzel]

#26113 (+340/-55): more API for monotone functions wrt topology

[Sébastien Gouëzel]

#26121 (+36/-13): more uses of simps in fiber bundles and vector bundles

[Jeremy Ravenel]

@Sébastien Gouëzel can I ask, is your use of convexity in relation to invariance of domain and the inverse function theorem?

[Sébastien Gouëzel]

The answer is no. The issue is that, even for a nice path-connected subset of $\R^2$ (say equal to the closure of its interior), the topology defined by the geodesic distance may be different from the topology defined by the original distance, if the set is not convex.

[Patrick Massot]

Jeremy, this is all about differential topology, not topological manifolds, so the invariance of domain has nothing to do here. Invariance of domain is crucial to ensure that topological manifolds have a (locally) unique dimension. But the analogous claim for differentiable manifolds trivially reduces to linear algebra because the differential of a diffeomorphism is a linear isomorphism.

[Sébastien Gouëzel]

Next PRs:

[Sébastien Gouëzel]

#26198 (+323/-2): change of variables formula in integrals for monotone functions.
This one should also be useful to @Yury G. Kudryashov for reparameterization of path integrals after #24754

[Sébastien Gouëzel]

#26197 (+244/-2): continuous Riemannian bundles
This one doesn't build currently, because the simpNF linter complains that it reaches a timeout in an unrelated lemma docs#ContinuousLinearMap.norm_smulRightL. Probably this means that I've made instance search slightly more costly, and that it's passed the threshold. I tried to improve things by making the instances I add with a very small priority, and to make several definitions reducible as in the reducible non-instances library note. To no avail. I don't know how to debug what is going on: if I create a new file importing all of mathlib and copy inside it the content of ContinuousLinearMap.norm_smulRightL, then everything is quick (no timeouts).

There is an easy but bad fix which is to just nolint simpNF this lemma, but it's probably not a good idea performancewise, because it means something fishy is going on somewhere. If anyone has an idea to improve the situation, I'm all ears. Otherwise, I'll go with my bad fix.

[Sébastien Gouëzel]

I've checked the timings, and they vary very little between before and after the PR. So in fact I think nolinting the lemma is the right thing to do. I've done it in the PR, which is now ready for review.

[Michael Rothgang]

Let me link a few more recent PRs, for easier finding:

[Michael Rothgang]

#26356 (+180/-173): refactor: move stuff on addition of iInf and iSup in ENNReal to a common place

[Michael Rothgang]

#26362 (+60/-15) preliminary refactoring; weaken assumption to NullMeasurableSet in some results on change of variables in integrals

[Michael Rothgang]

#26361 (+23) the function smoothTransition is monotone

[Michael Rothgang]

#26355 (+690/-290) add fun_ versions of many lemmas about one-dimensional derivatives

[Michael Rothgang]

Michael Rothgang said:

#26355 (+679/-288) add fun_ versions of many lemmas about one-dimensional derivatives

currently doesn't pass CI yet; I maintainer merge'd an old version: taking a look now Everything builds and tests fine; ought to lint.
Re-reviewed everything, still looks good.

[Michael Rothgang]

#26411 (+44/-0): add iInf results on ENNReal, matching existing iSup ones

[Winston Yin (尹維晨)]

May I just say a big thank you for this massive undertaking. Been looking forward to this for a long time!

[Sébastien Gouëzel]

Here is a new list of PRs, to keep the reviewers busy :-)

[Sébastien Gouëzel]

#26500 (+206/-2): more properties of the manifold structure on Icc

[Sébastien Gouëzel]

#26501 (+65/-7): more API on manifolds

[Sébastien Gouëzel]

#26502 (+49/-10): monotonicity of lineMap

[Sébastien Gouëzel]

#26503 (+77/-0): constructor for emetric space with a preexisting topology

[Sébastien Gouëzel]

#26504 (+34/-3): the image of an interval under a continuous monotone map is an interval

[Sébastien Gouëzel]

#26505 (+244/-1): in a continuous Riemannian bundle, the trivialization at a point is locally bounded in norm

[Sébastien Gouëzel]

#26506 (+201/-0): smooth Riemannian bundles

[Sébastien Gouëzel]

Again I'm really aware that this is a long list. The good news is that the final target in the list, #25347, builds fully and contains the theorem I wanted to prove (the distance coming from a Riemannian metric is indeed a distance, and it defines the same topology as the original one). This proves that the API is working fine to prove nontrivial results, so all that is left is to integrate all this into mathlib.

[Michael Rothgang]

No worries; I'm glad Patrick and I have some work to do again :-)

[Patrick Massot]

@Sébastien Gouëzel could you clarify the current status of this effort? Do you intend to cut #25347 into more pieces? Or are you now expecting a review? Note it still has the WIP label.

[Sébastien Gouëzel]

I'm still cutting it into pieces, hence the WIP. The next one is #26778.

[Sébastien Gouëzel]

And many thanks for all the reviews, this is getting merged to mathlib at a really impressive pace!

[Patrick Massot]

It really really help that Michael and I are both in Orsay with time and the explicit goal of doing differential geometry.

[Patrick Massot]

This allows us to stay focused on this area and not forget the big picture while moving from one PR to the next, and presumably it’s the same for you as an author.

[Patrick Massot]

In an ideal world this would be the situation for every big push to a specific area of Mathlib.

[Patrick Massot]

Being able to talk to another reviewer while reviewing is really helpful.

[Michael Rothgang]

I very much agree: the past weeks are quite possibly my most productive ones this year.

[Michael Rothgang]

I wonder if organising a "mathlib differential geometry workshop", where people come together for e.g. a week with the explicit goal of making progress would help. (Though being in Orsay for several weeks really helps; one week might possibly be too short.)
Or should we have differential geometry parties, to meet virtually and e.g. review a stack of PRs, or discuss difficult issues? (Lower barrier to entry, can be repeated more often, but same-room-ness is harder to approximate online.)

[Johan Commelin]

I think topical workshops are great! We've had several in the algebraic geometry corner of maths, and they were very productive.

[Kevin Buzzard]

We had a very productive algebraic geometry workshop at AIM in California, you could try for a differential geometry one. I didn't really want to go to California so we had it online. The cohomology workshop in Banff was in person though.

[Dominic Steinitz]

I would love a differential geometry workshop. Also I have my metric and connections (the usual Levi-Civita and what I call the Mercator connection) ready to try out via Christoffel symbols (for the metric) and connection coefficients (for the connections) :-)

[Kevin Buzzard]

I think that one thing which made the algebraic geometry workshop so interesting was that as well as lean experts in algebraic geometry there were also people like Ravi Vakil who knew less about lean but had very clear ideas about what theories should be developed and in what order. So if you go for it I would definitely sell it as being appropriate for differential geometers even if they know no lean and then just make sure internally that the lean diff geom experts can all make it

[Sébastien Gouëzel]

The final PR integrating Riemannian manifolds in Mathlib is ready for review, at #25347. It's a little bit long because it mixes a part on definitions, and a part proving a non-trivial theorem (the topology coming from the distance associated to a Riemannian metric coincides with the initial topology). I could split it in two, but I think that proving a nontrivial theorem shows that the design just works. Tell me if you want me to split it!

And many thanks to the reviewers who have already looked at a lot of PRs for this project!

[Patrick Massot]

@Sébastien Gouëzel could you move that branch to your fork?

[Sébastien Gouëzel]

Sure. #27250.

[Patrick Massot]

Ok, now both versions have comments…