feat: Naturality of integral curves #9341

winstonyin · 2023-12-29T22:02:38Z

Let v and v' be sections of the tangent bundle of manifolds M and M', respectively, and let f : M → M' be a differentiable map. Then f maps integral curves of v to integral curves of v' if and only if v and v' are f-related.

depends on: [Merged by Bors] - feat: local existence of integral curves of vector field #8483

- use lowerCamelCase for our definitions, per the naming convention. - sketch how to prove a few more sorries.

all results in this file hold for topological manifolds.

…e disjoint.

…ion. The current lemma (frontier of (e.extend I).target) has contributions from boundary(I.range) (good), but also from another factor (bad).

we should ask for x not being an interior of its chart's target. (Asking for "lies in the frontier", as we did before, would also include boundary points of (extChartAt I x).source in interior (range I), which we're not interested in.) In other words, the previous definition was actually *wrong*.

- make some variables explicit; fix namespacing of one result. - move all topology helper results into their own section.

grunweg

Took a preliminary look: looks pretty good to me. I would define f-relatedness, a new minor comments and then, once the dependent PR has been merged, it's good to go from my side.

If you want: add the Lie bracket under f-relatedness as a future TODO.

Mathlib/Geometry/Manifold/IntegralCurve.lean

grunweg · 2024-01-08T15:20:31Z

Mathlib/Geometry/Manifold/IntegralCurve.lean

+
+/-- Let `v` and `v'` be vector fields on `M` and `M'`, respectively, and let `f : M → M'` be a
+  differentiable map. If `v` and `v'` are `f`-related, then `f` maps integral curves of `v` to
+  integral curves of `v'`. The converse is stated below. -/


This is scope creep, but... how about introducing a definition of f-related vector fields? (I don't mind any somewhat interesting API being out of scope, but the definition would be useful, I think.)

Mathlib/Geometry/Manifold/IntegralCurve.lean

grunweg · 2024-01-08T15:24:28Z

Mathlib/Geometry/Manifold/IntegralCurve.lean

+    ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀ :=
+  exists_isIntegralCurveAt_of_contMDiffAt t₀ hv (BoundarylessManifold.isInteriorPoint I)
+
+section Naturality


Can you add a doc-string to this section, and - more importantly, mention this result in the high-level docstring?

Yes of course! If we're going to introduce f-relatedness and so on, which will be in a different file, this section should probably also go in a different file.

grunweg · 2024-01-08T15:31:42Z

I just realised: defining f-relatedness might entail defining vector fields as well. Sorry. I think this would be a great addition as well.

leanprover-community-mathlib4-bot · 2024-01-09T02:39:19Z

This PR/issue depends on:

~~[Merged by Bors] - feat: local existence of integral curves of vector field #8483~~
By Dependent Issues (🤖). Happy coding!

…rality

winstonyin · 2024-01-09T04:29:21Z

I agree with the need for new definitions. There's already ContMDiffSection, which we can perhaps generalise. I'll think about this another day.

…rality

github-actions · 2024-08-27T21:05:04Z

PR summary 1355af371a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ IsIntegralCurveAt.of_mdifferentiable_related
+ comp_smulRight
+ mdifferentiable_related_of_isIntegralCurveAt

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

winstonyin and others added 30 commits November 13, 2023 15:00

doc

4e53e96

compiles

f14b378

indent

22b4f1f

import, indent

0747174

docstring

23d691f

Mathlib.lean

e8e7338

lake manifest

ccc8f77

Merge remote-tracking branch 'origin/master' into integral_curve

42341d1

removed temporary notation

720ec35

integralCurveAt, change PicardLindelof statement order

25f1065

compiles

d4139b6

Sketch a section on interior and boundary of manifolds.

4b57dfe

More progress. Tweaks, polish and fleshing out some sorries.

e9d3546

- use lowerCamelCase for our definitions, per the naming convention. - sketch how to prove a few more sorries.

One more lemma.

cbd22f4

One lemma was in mathlib. :-)

0dbf3b0

Fix the build; mild clean-ups.

a978f02

Small simplifications.

1f6dbaa

has -> is, docstring, shift/stretch lemmas

9c58652

detailed proof steps

6b55cbc

open Set

0ada08e

IsIntegralCurveAt in preamble

063822d

IsIntegralCurveAt.comp_add

fb4196f

translation, scale, and reverse lemmas

6f665ad

iff lemmas

b59c82f

Small polish. Note that smoothness is not required;

3c2e424

all results in this file hold for topological manifolds.

The boundary is closed: entails showing that interior and boundary ar…

c95243e

…e disjoint.

Almost-proof that boundary has empty interior: need to adjust definit…

933cc59

…ion. The current lemma (frontier of (e.extend I).target) has contributions from boundary(I.range) (good), but also from another factor (bad).

Fix and complete proof that the boundary has empty interior.

f1fda32

Small clean-ups:

6a4e39c

- make some variables explicit; fix namespacing of one result. - move all topology helper results into their own section.

winstonyin added awaiting-review t-differential-geometry labels Dec 29, 2023

leanprover-community-mathlib4-bot added the blocked-by-other-PR label Dec 29, 2023

simp can prove this

78800db

leanprover-community-mathlib4-bot added the merge-conflict label Jan 5, 2024

winstonyin added 2 commits January 5, 2024 11:09

Merge remote-tracking branch 'origin/master' into integral_curve

ca88b9d

Merge branch 'integral_curve' into integral_curve_naturality

1997cb9

leanprover-community-mathlib4-bot removed the merge-conflict label Jan 5, 2024

winstonyin added 2 commits January 5, 2024 11:39

BoundarylessManifold

c74e830

Merge branch 'integral_curve' into integral_curve_naturality

15194c2

grunweg reviewed Jan 8, 2024

View reviewed changes

leanprover-community-mathlib4-bot removed the blocked-by-other-PR label Jan 9, 2024

leanprover-community-mathlib4-bot added the merge-conflict label Jan 9, 2024

Merge remote-tracking branch 'origin/master' into integral_curve_natu…

846fa99

…rality

leanprover-community-mathlib4-bot removed the merge-conflict label Jan 9, 2024

fix

69a2c47

minor

fceb0ee

grunweg added awaiting-author and removed awaiting-review labels Jan 9, 2024

Merge remote-tracking branch 'origin/master' into integral_curve_natu…

2a51584

…rality

leanprover-community-mathlib4-bot added the merge-conflict label Jan 23, 2024

winstonyin mentioned this pull request Jan 31, 2024

[Merged by Bors] - feat: uniform time lemma for the existence of global integral curves #9013

Closed

3 tasks

Merge remote-tracking branch 'origin/master' into integral_curve_natu…

830ad3a

…rality

CompleteSpace E

1355af3

leanprover-community-bot-assistant removed the merge-conflict label Aug 30, 2024

leanprover-community-bot-assistant added the merge-conflict label Nov 12, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Naturality of integral curves #9341

feat: Naturality of integral curves #9341

winstonyin commented Dec 29, 2023 •

edited by Parcly-Taxel

Loading

grunweg left a comment •

edited

Loading

grunweg Jan 8, 2024

grunweg Jan 8, 2024

winstonyin Jan 9, 2024

grunweg commented Jan 8, 2024

leanprover-community-mathlib4-bot commented Jan 9, 2024

winstonyin commented Jan 9, 2024

github-actions bot commented Aug 27, 2024 •

edited

Loading

Declarations diff

feat: Naturality of integral curves #9341

Are you sure you want to change the base?

feat: Naturality of integral curves #9341

Conversation

winstonyin commented Dec 29, 2023 • edited by Parcly-Taxel Loading

grunweg left a comment • edited Loading

Choose a reason for hiding this comment

grunweg Jan 8, 2024

Choose a reason for hiding this comment

grunweg Jan 8, 2024

Choose a reason for hiding this comment

winstonyin Jan 9, 2024

Choose a reason for hiding this comment

grunweg commented Jan 8, 2024

leanprover-community-mathlib4-bot commented Jan 9, 2024

winstonyin commented Jan 9, 2024

github-actions bot commented Aug 27, 2024 • edited Loading

PR summary 1355af371a

Import changes for modified files

Declarations diff

winstonyin commented Dec 29, 2023 •

edited by Parcly-Taxel

Loading

grunweg left a comment •

edited

Loading

github-actions bot commented Aug 27, 2024 •

edited

Loading