[Merged by Bors] - feat: local existence of integral curves of vector field #8483
Conversation
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
leanprover-community-mathlib4-bot
added
the
merge-conflict
winstonyin
removed
the
merge-conflict
There was a problem hiding this comment.
I know this is still work in progress - I still have some comments and suggestions, perhaps they're helpful. As with the other PR: I'm really glad you're working on this! Don't let my number of comments discourage you; rather take that as a sign that I read your code closely :-)
I haven't looked at the big proof in detail yet.
|
(Taking the liberty to tag this as differential geometry; hope you don't mind.) I think the definition of interior and boundary of a manifold would make a nice little section; would you be interested if I try to flesh that out a little? (For instance, I could push a commit to your PR, or make a separate PR with you as co-author.) |
FYI, I started a section outlining these things on a branch. I think that is close to the right abstraction for mathlib; a number of sorries are still open. If you'd like, we can join forces in filling them in :-). |
|
I’d love to work together on this. You should just push to my branch! Thanks for all the detailed comments :) |
|
I just pushed a commit with my skeleton for interior and boundary. I'll work a little while more on it (30mins perhaps), then I'll leave it to you. By the way, did you forget to push local changes? Edit: done for today; feel free to take over! |
- use lowerCamelCase for our definitions, per the naming convention. - sketch how to prove a few more sorries.
|
Yes I did forget to push local changes. Will merge them with your commits! |
We define `tangentCoordChange` as a convenient abbreviation for coordinate changes on the tangent bundle. We also restate the axioms of `VectorBundleCore` as lemmas involving `extChartAt`. Currently, we need to write `(tangentBundleCore I M).coordChange (achart H x) (achart H y)`, referring explicitly to the atlas of `M`. Since `tangentBundleCore` uses the same base sets as the preferred charts of the base manifold, we wish to work directly with points `x y : M` and the preferred extended charts at those points (`extChartAt`). We find this definition and related lemmas useful in #8483 in shortening proofs.
We define `tangentCoordChange` as a convenient abbreviation for coordinate changes on the tangent bundle. We also restate the axioms of `VectorBundleCore` as lemmas involving `extChartAt`. Currently, we need to write `(tangentBundleCore I M).coordChange (achart H x) (achart H y)`, referring explicitly to the atlas of `M`. Since `tangentBundleCore` uses the same base sets as the preferred charts of the base manifold, we wish to work directly with points `x y : M` and the preferred extended charts at those points (`extChartAt`). We find this definition and related lemmas useful in #8483 in shortening proofs.
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
And I just pushed a comment making I in |
|
✌️ winstonyin can now approve this pull request. To approve and merge a pull request, simply reply with |
| local integral curve of `v` in a neighbourhood containing `t₀`. The value of `γ` outside of this | ||
| interval is irrelevant and considered junk. -/ | ||
| def IsIntegralCurveAt (γ : ℝ → M) (v : (x : M) → TangentSpace I x) (t₀ : ℝ) : Prop := | ||
| ∀ᶠ t in 𝓝 t₀, HasMFDerivAt 𝓘(ℝ, ℝ) I γ t ((1 : ℝ →L[ℝ] ℝ).smulRight <| v (γ t)) |
There was a problem hiding this comment.
This is now stated in terms of Filter.Eventually to make the three definitions more symmetric.
| lemma isIntegralCurve_iff_isIntegralCurveOn : IsIntegralCurve γ v ↔ IsIntegralCurveOn γ v univ := | ||
| ⟨fun h ↦ h.isIntegralCurveOn _, fun h t ↦ h t (mem_univ _)⟩ | ||
|
|
||
| lemma isIntegralCurveAt_iff : |
There was a problem hiding this comment.
The lemma @ocfnash suggested above, before I changed the definition of IsIntegralCurveAt.
|
Merging this now, moving on to #8886! If there's disagreement on the last-minute change in It's hard to overstate how happy I am that this is getting merged. It's my first new file / new API! I finished the first draft of this over a year ago (before the port began), and the detailed reviews by @grunweg and @ocfnash have been very supportive and encouraging. Thank you! bors r+ |
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]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Port of mathlib#17140 plus much more. Comments therein addressed.
For any continuously differentiable vector field (section of tangent bundle) on a manifold
Mand any chosen interior pointx₀ : M, there exists an integral curveγ : ℝ → Msuch thatγ t₀ = x₀for any real numbert₀and the tangent vector ofγattcoincides with the vector field atγ tfor alltwithin an open interval aroundt₀.As a corollary, such an integral curve exists for any starting point
x₀ifMis a manifold without boundary.We define three
Props:IsIntegralCurveOn γ v smeansγ tis tangent tov (γ t)for alltwithins : Set ℝ.IsIntegralCurveAt γ v t₀meansγis a local integral curve tov. That is,γ tis tangent tov (γ t)for alltwithin some open interval oft₀.IsIntegralCurve γ vmeansγis a global integral curve tov. That is,γ tis tangent tov (γ t)for allt : ℝ.Lemmas about rescaling and translation of integral curves are proven:
γsolvesvatt₀, thenγ (t + dt)is tangent tovatt₀ - dt.γsolvesvatt₀, thenγ (a * t)is tangent toa • vatt₀ / afor any non-zeroa.x₀solves anyvwithv x₀ = 0.We also shuffle the position of
∃ ε > (0 : ℝ)inPicardLindelofto one that makes more sense, sincef t₀ = x₀does not depend onεyet.