[Merged by Bors] - feat: uniform time lemma for the existence of global integral curves #9013
Conversation
That's the normal form (and conceptually simpler); jumping between these different forms means I need to rewrite more often. Most of the time, I don't care which one I use. Delete a helper lemma about this bad normal form: shouldn't use that.
mathlib has a related version, with a slightly different formula...
Extracting all those tiny lemmas still feels slightly weird, but I guess they are still useful, somewhen. apply? cannot find them, at least.
I don't see how to show this, given the current hypotheses.
I decided two MapsTo helpers are obvious enough to be left out, but disjointness of interior and frontier is interesting enough.
Everything else requires advanced technology not in mathlib yet.
…ity/mathlib4 into integral_curve
And combine some apply lines.
Golf proofs about composition of integral curves.
…ation lemmas for subtraction (#19008) We restate the translation lemmas for integral curves using the `Pointwise` API and add translation lemmas for subtraction for convenience. This is just split out from #9013. The `Pointwise` API allows us to use lemmas like `Metric.vadd_ball` and more convenient rewriting of the `dt` term (rather than rewriting it inside the set builder notation).
|
@grunweg I remember what the issue is with proving the existence of global integral curves on compact manifolds. We need that the solution to ODEs is smooth wrt the initial conditions. I'm not sure we have that in mathlib yet. One standard proof of this relies on an integral over a finite-dimensional space, so to be general, we also need that compact differentiable manifolds are finite-dimensional. Seems like a fun excursion through mathlib which I may or may not have time for. |
|
Fun excursions are always nice. (I have an ever-growing list of these myself. But that means every time somebody ask "do you have a nice Lean project in mind", I have an answer :-)) I'd be happy to review, if you get there! About smoothness: doesn't the manifold version simply follow from the statement in normed spaces? And that version should certainly be in mathlib (though I haven't checked). Put differently: I wouldn't mind merging a PR stating this for compact finite-dimensional manifolds, with a TODO that fin-dim is implied, so should be removed later. |
There was a problem hiding this comment.
Thanks, I like this version much better!
Reading the code, there are tedious details about discharging all the arithmetic side conditions. I do wonder if this can be golfed, but don't see a way immediately. Let's ask for some maintainer feedback! Thanks for sticking with this PR, I'm very happy it is getting into mathlib now.
maintainer merge?
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
If you can find the smooth dependence on initial conditions, please tell me where! I'm almost done proving that locally compact manifolds are finite-dimensional (using Riesz's theorem). |
| (γ : ℝ → ℝ → M) (hγx : ∀ a, γ a 0 = x) (hγ : ∀ a, IsIntegralCurveOn (γ a) v (Ioo (-a) a)) | ||
| {a a' : ℝ} (hpos : 0 < a') (hle : a' ≤ a) : | ||
| EqOn (γ a') (γ a) (Ioo (-a') a') := by |
There was a problem hiding this comment.
- Would it make sense to use
epsilons instead ofas here? What is the convention? - In
hγI think you can make the condition weaker by requiring this only forathat are> 0. That might make it a bit easier to check the condition, but requires a bit more work in the current proof. If you think this lemma will be applied several times, it might be worth it.
There was a problem hiding this comment.
I don't know the convention very well either, but I don't think epsilon makes sense here: a is any real number, not a "small" one. One could use t instead of a (no strong opinion).
Right now, this lemma is just used once (in one proof, twice). I'm not sure if there will be further uses. Perhaps, when speaking about the existence of geodesics... (which are a bit away, as mathlib is missing Riemannian metrics, hence the exponential map). What do you think @winstonyin?
There was a problem hiding this comment.
But at the place where it is used, the same assumption is in place, so the weakening could propagate.
There was a problem hiding this comment.
I just pushed a commit doing this. Overall, the code gets a bit longer. What do you think?
| (γ : ℝ → ℝ → M) (hγx : ∀ a, γ a 0 = x) (hγ : ∀ a, IsIntegralCurveOn (γ a) v (Ioo (-a) a)) | ||
| {a a' : ℝ} (hpos : 0 < a') (hle : a' ≤ a) : | ||
| EqOn (γ a') (γ a) (Ioo (-a') a') := by |
There was a problem hiding this comment.
I don't know the convention very well either, but I don't think epsilon makes sense here: a is any real number, not a "small" one. One could use t instead of a (no strong opinion).
Right now, this lemma is just used once (in one proof, twice). I'm not sure if there will be further uses. Perhaps, when speaking about the existence of geodesics... (which are a bit away, as mathlib is missing Riemannian metrics, hence the exponential map). What do you think @winstonyin?
jcommelin
added
awaiting-author
grunweg
removed
the
awaiting-author
|
This seems ready for review again. |
|
Thanks 🎉 bors merge |
leanprover-community-mathlib4-bot
added
the
ready-to-merge
…9013) Lemma 9.15 in Lee's Introduction to Smooth Manifolds: > Let `v` be a smooth vector field on a smooth manifold `M`. If there exists `ε > 0` such that for each point `x : M`, there exists an integral curve of `v` through `x` defined on an open interval `Ioo (-ε) ε`, then every point on `M` has a global integral curve of `v` passing through it. We only require `v` to be $C^1$. To achieve this, we define the extension of an integral curve `γ` by another integral curve `γ'`, if they agree at a point inside their overlapping open interval domains. This utilises the uniqueness theorem of integral curves. We need this lemma to show that vector fields on compact manifolds always have global integral curves. - [x] depends on: #8886 - [x] depends on: #18833 - [x] depends on: #19008 Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Johan Commelin <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Lemma 9.15 in Lee's Introduction to Smooth Manifolds:
We only require$C^1$ .
vto beTo achieve this, we define the extension of an integral curve
γby another integral curveγ', if they agree at a point inside their overlapping open interval domains. This utilises the uniqueness theorem of integral curves.We need this lemma to show that vector fields on compact manifolds always have global integral curves.
IntegralCurve#18833