feat(geometry/manifold): Integral curve of vector fields #17140
Conversation
mathlib-dependent-issues-bot
added
the
blocked-by-other-PR
| at `t` coincides with the vector field at `γ t` for all `t` within an open interval around 0.-/ | ||
| theorem exists_integral_curve_of_cont_mdiff_tangent_vector_field [proper_space E] | ||
| (v : M → tangent_bundle I M) (h₁ : ∀ x, (v x).1 = x) (h₂ : cont_mdiff I I.tangent 1 v) | ||
| (x₀ : M) (hx : 𝓔(I, x₀) x₀ ∈ interior 𝓔(I, x₀).target) : |
There was a problem hiding this comment.
Instead of hx, I'd rather define a predicate saying that x₀ is a non-boundary point, and use that here and in the other statements above.
There was a problem hiding this comment.
Implemented! I also added t₀ as an argument so it is not assumed to be =0.
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
winstonyin
added
awaiting-review
|
GitHub is showing some changes that already landed as part of #16348
|
| /-- An interior point of a manifold is a point whose image in the model vector space is in the | ||
| interior of the chart's target. | ||
|
|
||
| TODO : This definition refers to a chosen chart at `x`, but the property is independent of the |
There was a problem hiding this comment.
It's not obvious to me that this doesn't depend on the choice of charts. For finite-dimensional real manifolds, yes, but for general manifolds over a general field maybe not?
There was a problem hiding this comment.
I'm only aware of the finite-dimensional real manifold case.
| [proper_space E] [I.boundaryless] | ||
| (h₁ : ∀ x, (v x).1 = x) (h₂ : cont_mdiff I I.tangent 1 v) (t₀ : ℝ) (x₀ : M) : | ||
| ∃ (ε > (0 : ℝ)) (γ : ℝ → M), γ t₀ = x₀ ∧ ∀ (t : ℝ), t ∈ set.Ioo (t₀ - ε) (t₀ + ε) → | ||
| has_mfderiv_at 𝓘(ℝ, ℝ) I γ t ((1 : ℝ →L[ℝ] ℝ).smul_right (𝓔(I.tangent, v(γ t)) (v (γ t))).2) := |
There was a problem hiding this comment.
The statement here is strange: the right statement should say that the derivative of gamma is v (gamma t) (with an smul_right as you do since we only have mfderiv and not mderiv), but there should be no chart in sight. My guess is that the difficulty comes from your choice for the type of v, as a general function from M to its tangent bundle (and then imposing that it's a section by putting a requirement (v x).1 = x). Instead, a section should probably be a function v : Π x, tangent_bundle I x: in this way, v x is by definition an element of the tangent bundle at x, and everything makes sense more easily.
Also, you are requiring that v should be C^1 globally, but the statement should be true if v is just C^1 around x.
Also, can you comment on the properness assumption on E? Cauchy-Lipschitz works in complete spaces, so I expect this assumption should be enough, right?
There is a difficulty here that we are undergoing a refactor of vector bundles currently. By the end of this refactor, we will probably have a nice API to speak of sections, smooth sections, and so on, but it's not the case currently. So I'm not sure what to advise on this PR. If you can make it work without too much trouble with the right statement and the current API, we can probably merge it now and refactor it when the vector bundle refactor lands. @hrmacbeth , @fpvandoorn , what are your thoughts on this?
There was a problem hiding this comment.
I'll try to rewrite the type of section v and see if charts can be removed. I'll also relax the C^1 condition on v.
The proof of exists_is_picard_lindelof_const_of_cont_diff_on_nhds, which states that locally C^1 vector fields have a local solution, needs ∥v x∥ to be bounded above for x in a closed ball. This uses is_compact.bdd_above_image, which needs proper_space E.
I'm really looking forward to the vector bundles refactor, as the current API has been rather tricky to work with. I'm happy to use this PR to get some maths comments (which you've very helpfully given) and then rewrite it using the new API when it's ready. How can I follow the progress of its development?
There was a problem hiding this comment.
Currently, the "top" of the vector bundle refactor is #17680, but that PR depends on 5 other open pull requests. The refactor has been moving very slowly, since both @hrmacbeth and I have been focusing more on other things recently (like mathlib4 porting).
There was a problem hiding this comment.
For ∥v x∥ to be bounded above in a small closed ball around a point x_0, you don't need properness: continuity at x_0 is enough.
sgouezel
added
awaiting-author
Port of [mathlib#17140](leanprover-community/mathlib3#17140) plus much more. Comments therein addressed. For any continuously differentiable vector field (section of tangent bundle) on a manifold `M` and any chosen interior point `x₀ : M`, there exists an integral curve `γ : ℝ → M` such that `γ t₀ = x₀` for any real number `t₀` and the tangent vector of `γ` at `t` coincides with the vector field at `γ t` for all `t` within an open interval around `t₀`. As a corollary, such an integral curve exists for any starting point `x₀` if `M` is a manifold without boundary. We define three `Prop`s: 1. `IsIntegralCurveOn γ v s` means `γ t` is tangent to `v (γ t)` for all `t` within `s : Set ℝ`. 2. `IsIntegralCurveAt γ v t₀` means `γ` is a local integral curve to `v`. That is, `γ t` is tangent to `v (γ t)` for all `t` within some open interval of `t₀`. 3. `IsIntegralCurve γ v` means `γ` is a global integral curve to `v`. That is, `γ t` is tangent to `v (γ t)` for all `t : ℝ`. Lemmas about rescaling and translation of integral curves are proven: * If `γ` solves `v` at `t₀`, then `γ (t + dt)` is tangent to `v` at `t₀ - dt`. * If `γ` solves `v` at `t₀`, then `γ (a * t)` is tangent to `a • v` at `t₀ / a` for any non-zero `a`. * The constant function at `x₀` solves any `v` with `v x₀ = 0`. We also shuffle the position of `∃ ε > (0 : ℝ)` in `PicardLindelof` to one that makes more sense, since `f t₀ = x₀` does not depend on `ε` yet. Co-authored-by: Michael Rothgang <[email protected]>
For any continuously differentiable vector field on a manifold
Mand any chosen non-boundary pointx₀ : M, an integral curveγ : ℝ → Mexists such thatγ 0 = x₀and the tangent vector ofγattcoincides with the vector field atγ tfor alltwithin an open interval around 0.As a corollary, such an integral curve exists for any starting point
x₀ifMis a manifold without boundary.We have proven and used a few lemmas which may be useful in
geometry.manifold.smooth_manifold_with_cornersandgeometry.manifold.tangent_bundle.Note: I'm not totally satisfied with the way the lemmas leading to the theorem are structured, so any suggestions for generalisation of lemmas or splitting the long proofs into further lemmas are very welcome.