Time-dependent flows on manifolds

A time-dependent vector field on a manifold M is a family X t of vector fields on M, indexed by the time t : ℝ. Its integral curves are the curves γ with γ' u = X u (γ u). Adjoining the clock equation t' = 1 turns X into the autonomous vector field (t, x) ↦ (1, X t x) on ℝ × M, its suspension (TauCeti.timeDependentSuspensionField), and the maximal flow of the suspension yields the maximal time-dependent flow of X: TauCeti.timeDependentFlowOf X s t x is the value at time t of the maximal integral curve of X which passes through x at time s. It is defined on the set TauCeti.timeDependentFlowDomain X of triples ((s, t), x), and is total, with junk values outside that set.

For a jointly C^n time-dependent field on a finite-dimensional boundaryless manifold, 1 ≤ n, this is the fundamental theorem on time-dependent flows: the domain is open and contains every triple ((s, s), x), the flow is jointly C^n on it, its curves t ↦ timeDependentFlowOf X s t x solve the equation and are the unique solutions through x at time s, and the two-time composition law holds wherever its terms are defined. A time-dependent field vanishing outside a compact subset of M at all times has a complete suspension, and then every time map is a C^n diffeomorphism of M, with inverse the time map in the opposite direction.

Compactly supported time-dependent fields are the input to the isotopy extension theorem: the velocity of a moving compact submanifold, extended to a compactly supported field on the ambient manifold, has a complete suspension, and its time maps are the ambient diffeomorphisms that carry the initial position of the submanifold to the later ones.

Main definitions

• TauCeti.timeDependentSuspensionField X: the autonomous field (t, x) ↦ (1, X t x) on ℝ × M.
• TauCeti.timeDependentFlowDomain X: the domain of the maximal time-dependent flow.
• TauCeti.timeDependentFlowOf X s t x: the maximal time-dependent flow from time s to time t.
• TauCeti.timeDependentFlowDiffeomorph: for a complete suspension, the time map from s to t as a C^n diffeomorphism.
• TauCeti.timeDependentFlowMFDerivEquiv: for a complete suspension, the differential of the time map as a continuous linear equivalence of tangent spaces.

Main results

• TauCeti.flowOf_timeDependentSuspensionField: the flow of the suspension advances the clock at unit speed and moves the point along the time-dependent flow.
• TauCeti.isOpen_timeDependentFlowDomain and TauCeti.contMDiffOn_timeDependentFlowOf: the domain is open and the flow is jointly C^n on it.
• TauCeti.hasMFDerivAt_timeDependentFlowOf: the curves of the flow solve γ' u = X u (γ u).
• TauCeti.timeDependentFlowOf_eq_of_hasMFDerivAt: every solution on an open interval is a curve of the flow.
• TauCeti.timeDependentFlowOf_trans_of_mem and TauCeti.timeDependentFlowOf_trans: the two-time composition law, where it is defined, and everywhere for a complete suspension.
• TauCeti.timeDependentFlowOf_symm_of_mem: flowing back from time t to time s undoes the flow from s to t.
• TauCeti.isCompleteVectorField_timeDependentSuspensionField: a time-dependent field vanishing outside a fixed compact set has a complete suspension.
• TauCeti.hasMFDerivAt_timeDependentFlowOf_comp: a map moved by the flow at a varying time, y ↦ timeDependentFlowOf X s (τ y) (v y), has derivative dφ ∘ dv + dτ ⊗ X.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Theorem 9.48 (the fundamental theorem on time-dependent flows).
• M. W. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §1 (isotopy extension by compactly supported time-dependent vector fields).

The formalization adapts the time-dependent flow construction of the Tau Ceti contributors (https://github.com/TauCetiProject/TauCeti/pull/20364).

The suspension construction is the manifold counterpart of TauCeti.timeDependentSuspension in TauCeti.Dynamics.Flow.TimeDependent; the maximal flow is Tau Ceti's TauCeti.flowOf.

The suspension of a time-dependent vector field

def TauCeti.timeDependentSuspensionField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] (X : ℝ → (x : M) → TangentSpace I x) (p : ℝ × M) : TangentSpace ((modelWithCornersSelf ℝ ℝ).prod I) p

The suspension of a time-dependent vector field X on M: the autonomous vector field (t, x) ↦ (1, X t x) on ℝ × M, whose first component advances the clock at unit speed.

@[simp]

theorem TauCeti.timeDependentSuspensionField_fst {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] (X : ℝ → (x : M) → TangentSpace I x) (p : ℝ × M) : (timeDependentSuspensionField X p).1 = 1

The clock component of the suspension is 1.

@[simp]

theorem TauCeti.timeDependentSuspensionField_snd {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] (X : ℝ → (x : M) → TangentSpace I x) (p : ℝ × M) : (timeDependentSuspensionField X p).2 = X p.1 p.2

The spatial component of the suspension at (t, x) is X t x.

theorem TauCeti.contMDiff_const_prod_field {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {X : ℝ → (x : M) → TangentSpace I x} (c : ℝ) (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) ((modelWithCornersSelf ℝ ℝ).prod I).tangent n fun (p : ℝ × M) => ⟨p, (c, X p.1 p.2)⟩

For a jointly C^n time-dependent vector field X and a real number c, the field (c, X) on ℝ × M is a C^n vector field. For c = 1 it is the suspension of X, for c = 0 it is the vertical field of X, and for X = 0 and c = 1 it is the unit field ∂_t of the time coordinate.

theorem TauCeti.contMDiff_timeDependentSuspensionField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {X : ℝ → (x : M) → TangentSpace I x} (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) ((modelWithCornersSelf ℝ ℝ).prod I).tangent n fun (p : ℝ × M) => ⟨p, timeDependentSuspensionField X p⟩

The suspension of a jointly C^n time-dependent vector field is a C^n vector field on ℝ × M.

The maximal time-dependent flow

def TauCeti.timeDependentFlowDomain {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] (X : ℝ → (x : M) → TangentSpace I x) : Set ((ℝ × ℝ) × M)

The domain of the maximal time-dependent flow of X: the triples ((s, t), x) such that the maximal integral curve of X through x at time s is defined at time t.

noncomputable def TauCeti.timeDependentFlowOf {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] (X : ℝ → (x : M) → TangentSpace I x) (s t : ℝ) (x : M) : M

The maximal time-dependent flow of X: timeDependentFlowOf X s t x is the value at time t of the maximal integral curve of X passing through x at time s. It is read off the maximal flow of the suspension of X, and has junk values outside timeDependentFlowDomain X.

theorem TauCeti.mem_timeDependentFlowDomain {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {x : M} : ((s, t), x) ∈ timeDependentFlowDomain X ↔ (t - s, s, x) ∈ flowDomain (timeDependentSuspensionField X)

Membership in the domain of the time-dependent flow is membership of (t - s, (s, x)) in the domain of the maximal flow of the suspension.

theorem TauCeti.timeDependentFlowOf_def {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {x : M} : timeDependentFlowOf X s t x = (flowOf (timeDependentSuspensionField X) (t - s) (s, x)).2

The time-dependent flow is the spatial component of the flow of the suspension.

Solutions of the time-dependent equation

theorem TauCeti.mem_timeDependentFlowDomain_of_hasMFDerivAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {γ : ℝ → M} {a b : ℝ} (hγ : ∀ u ∈ Set.Ioo a b, HasMFDerivAt% γ u (ContinuousLinearMap.smulRight 1 (X u (γ u)))) (hs : s ∈ Set.Ioo a b) (ht : t ∈ Set.Ioo a b) : ((s, t), γ s) ∈ timeDependentFlowDomain X

A solution γ of the time-dependent equation on an open interval containing s and t stays in the domain of the time-dependent flow: ((s, t), γ s) lies in it.

theorem TauCeti.mem_timeDependentFlowDomain_of_forall_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {x : M} (hx : ∀ (u : ℝ), X u x = 0) (s t : ℝ) : ((s, t), x) ∈ timeDependentFlowDomain X

A point at which X vanishes at all times stays in the domain of the time-dependent flow.

theorem TauCeti.ordConnected_setOf_mem_timeDependentFlowDomain {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (s : ℝ) (x : M) : {u : ℝ | ((s, u), x) ∈ timeDependentFlowDomain X}.OrdConnected

The times at which the flow from (s, x) is defined form an interval.

theorem TauCeti.exists_Ioo_of_mem_timeDependentFlowDomain {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {x : M} (h : ((s, t), x) ∈ timeDependentFlowDomain X) : ∃ (a : ℝ) (b : ℝ), s ∈ Set.Ioo a b ∧ t ∈ Set.Ioo a b ∧ ∀ u ∈ Set.Ioo a b, ((s, u), x) ∈ timeDependentFlowDomain X

Two times at which the flow from (s, x) is defined, s and t, lie in a common open interval of times at which it is defined.

theorem TauCeti.fst_flowOf_timeDependentSuspensionField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s : ℝ} {x : M} {τ : ℝ} (hτ : (τ, s, x) ∈ flowDomain (timeDependentSuspensionField X)) : (flowOf (timeDependentSuspensionField X) τ (s, x)).1 = s + τ

The clock of the suspension runs at unit speed. Along the maximal integral curve of the suspension through (s, x), the time coordinate at flow time τ is s + τ.

theorem TauCeti.flowOf_timeDependentSuspensionField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {x : M} (h : ((s, t), x) ∈ timeDependentFlowDomain X) : flowOf (timeDependentSuspensionField X) (t - s) (s, x) = (t, timeDependentFlowOf X s t x)

The flow of the suspension through (s, x) reaches the point (t, timeDependentFlowOf X s t x) after time t - s.

@[simp]

theorem TauCeti.timeDependentFlowOf_self {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] (X : ℝ → (x : M) → TangentSpace I x) (s : ℝ) (x : M) : timeDependentFlowOf X s s x = x

The time-dependent flow from time s to time s is the identity.

theorem TauCeti.mem_timeDependentFlowDomain_self_of_mem {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {x : M} (h : ((s, t), x) ∈ timeDependentFlowDomain X) : ((s, s), x) ∈ timeDependentFlowDomain X

If a triple ((s, t), x) lies in the domain of the time-dependent flow, so does ((s, s), x).

theorem TauCeti.hasMFDerivAt_timeDependentFlowOf {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (h : ((s, t), x) ∈ timeDependentFlowDomain X) : HasMFDerivAt% (fun (u : ℝ) => timeDependentFlowOf X s u x) t (ContinuousLinearMap.smulRight 1 (X t (timeDependentFlowOf X s t x)))

The curves of the time-dependent flow solve the equation. At every time t at which it is defined, the curve u ↦ timeDependentFlowOf X s u x has velocity X t (timeDependentFlowOf X s t x).

theorem TauCeti.timeDependentFlowOf_eq_of_hasMFDerivAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) {γ : ℝ → M} {a b : ℝ} (hγ : ∀ u ∈ Set.Ioo a b, HasMFDerivAt% γ u (ContinuousLinearMap.smulRight 1 (X u (γ u)))) (hs : s ∈ Set.Ioo a b) (ht : t ∈ Set.Ioo a b) : timeDependentFlowOf X s t (γ s) = γ t

Uniqueness of solutions. A solution γ of the time-dependent equation on an open interval containing s and t is the curve of the time-dependent flow through γ s at time s.

theorem TauCeti.timeDependentFlowOf_eq_self_of_forall_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (hx : ∀ (u : ℝ), X u x = 0) (s t : ℝ) : timeDependentFlowOf X s t x = x

A point at which X vanishes at all times is fixed by the time-dependent flow.

theorem TauCeti.timeDependentFlowOf_trans_of_mem {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) {r : ℝ} (hrs : ((r, s), x) ∈ timeDependentFlowDomain X) (hst : ((s, t), timeDependentFlowOf X r s x) ∈ timeDependentFlowDomain X) : ((r, t), x) ∈ timeDependentFlowDomain X ∧ timeDependentFlowOf X s t (timeDependentFlowOf X r s x) = timeDependentFlowOf X r t x

The two-time composition law. Flowing from time r to time s and then from s to t is flowing from r to t, provided both steps are defined; the composite is then defined.

theorem TauCeti.isOpen_timeDependentFlowDomain {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) [FiniteDimensional ℝ E] : IsOpen (timeDependentFlowDomain X)

In finite dimensions, the domain of the time-dependent flow of a C¹ field is open.

theorem TauCeti.contMDiffOn_timeDependentFlowOf {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) : ContMDiffOn (((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ ℝ)).prod I) I (↑n) (fun (p : (ℝ × ℝ) × M) => timeDependentFlowOf X p.1.1 p.1.2 p.2) (timeDependentFlowDomain X)

In finite dimensions, the time-dependent flow of a C^n field, 1 ≤ n, is jointly C^n in the initial time, the final time and the initial point on its domain.

theorem TauCeti.mem_timeDependentFlowDomain_self {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s : ℝ) (x : M) : ((s, s), x) ∈ timeDependentFlowDomain X

Every triple ((s, s), x) lies in the domain of the time-dependent flow.

theorem TauCeti.timeDependentFlowOf_mem_insert {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {x : M} [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) [T2Space M] {K : Set M} (hXK : ∀ (u : ℝ), ∀ y ∉ K, X u y = 0) (h : ((s, t), x) ∈ timeDependentFlowDomain X) : timeDependentFlowOf X s t x ∈ insert x K

Under a time-dependent field vanishing outside K at all times, the time-dependent flow keeps every point in K together with its initial point.

theorem TauCeti.isCompleteVectorField_timeDependentSuspensionField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} [CompleteSpace E] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) [T2Space M] {K : Set M} (hK : IsCompact K) (hXK : ∀ (u : ℝ), ∀ y ∉ K, X u y = 0) : IsCompleteVectorField (timeDependentSuspensionField X)

A time-dependent field vanishing outside a fixed compact set has a complete suspension. The field may depend arbitrarily on time, and its suspension need not have compact support in the time direction.

theorem TauCeti.timeDependentFlowOf_symm_of_mem {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} {s t : ℝ} {x : M} [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) [T2Space M] (h : ((s, t), x) ∈ timeDependentFlowDomain X) : ((t, s), timeDependentFlowOf X s t x) ∈ timeDependentFlowDomain X ∧ timeDependentFlowOf X t s (timeDependentFlowOf X s t x) = x

Flowing back undoes the flow. If the flow from time s to time t is defined at x, then the flow from t back to s is defined at its endpoint and returns it to x.

theorem TauCeti.exists_timeDependentFlow {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} [FiniteDimensional ℝ E] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s : ℝ) (x : M) : ∃ (U : Set (ℝ × M)) (Ψ : ℝ → ℝ × M → M), IsOpen U ∧ (s, x) ∈ U ∧ (∀ p ∈ U, Ψ p.1 p = p.2) ∧ ∀ p ∈ U, ∀ᶠ (t : ℝ) in nhds p.1, HasMFDerivAt% (fun (u : ℝ) => Ψ u p) t (ContinuousLinearMap.smulRight 1 (X t (Ψ t p)))

A jointly C¹ time-dependent field on a finite-dimensional boundaryless manifold has a local flow through every time and point. The solution through (s, x) starts at x at time s and solves the nonautonomous equation for all times sufficiently close to s.

Complete suspensions

theorem TauCeti.timeDependentFlowDomain_eq_univ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) : timeDependentFlowDomain X = Set.univ

If the suspension is complete, the time-dependent flow is defined everywhere.

theorem TauCeti.timeDependentFlowOf_trans {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (r s t : ℝ) (x : M) : timeDependentFlowOf X s t (timeDependentFlowOf X r s x) = timeDependentFlowOf X r t x

If the suspension is complete, flowing from time r to time s and then from s to t is flowing from r to t.

theorem TauCeti.contMDiff_timeDependentFlowOf {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) : ContMDiff (((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ ℝ)).prod I) I ↑n fun (p : (ℝ × ℝ) × M) => timeDependentFlowOf X p.1.1 p.1.2 p.2

If the suspension of a C^n time-dependent field, 1 ≤ n, on a finite-dimensional manifold is complete, its time-dependent flow is jointly C^n in both times and the initial point.

noncomputable def TauCeti.timeDependentFlowDiffeomorph {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s t : ℝ) : Diffeomorph I I M M ↑n

If the suspension of a C^n time-dependent field, 1 ≤ n, on a finite-dimensional manifold is complete, the time-dependent flow from time s to time t is a C^n diffeomorphism, with inverse the time-dependent flow from t to s.

@[simp]

theorem TauCeti.timeDependentFlowDiffeomorph_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s t : ℝ) (x : M) : (timeDependentFlowDiffeomorph hcomplete hn hX s t) x = timeDependentFlowOf X s t x

The diffeomorphism timeDependentFlowDiffeomorph is the time-dependent flow.

@[simp]

theorem TauCeti.timeDependentFlowDiffeomorph_symm_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s t : ℝ) (x : M) : (timeDependentFlowDiffeomorph hcomplete hn hX s t).symm x = timeDependentFlowOf X t s x

The inverse of timeDependentFlowDiffeomorph from s to t is the time-dependent flow from t to s.

noncomputable def TauCeti.timeDependentFlowMFDerivEquiv {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s t : ℝ) (x : M) : TangentSpace I x ≃L[ℝ] TangentSpace I (timeDependentFlowOf X s t x)

The linearized time-dependent flow: if the suspension of a C^n time-dependent field, 1 ≤ n, is complete, the differential of the flow from s to t at x is a continuous linear equivalence T_x M ≃ T_{φ_{s,t} x} M, with inverse the differential of the flow from t to s.

@[simp]

theorem TauCeti.coe_timeDependentFlowMFDerivEquiv {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s t : ℝ) (x : M) : ↑(timeDependentFlowMFDerivEquiv hcomplete hn hX s t x) = mfderiv% (timeDependentFlowOf X s t) x

The linearized time-dependent flow is the differential of the time map.

@[simp]

theorem TauCeti.timeDependentFlowMFDerivEquiv_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s t : ℝ) (x : M) (v : TangentSpace I x) : (timeDependentFlowMFDerivEquiv hcomplete hn hX s t x) v = (mfderiv% (timeDependentFlowOf X s t) x) v

The linearized time-dependent flow applies the differential of the time map.

@[simp]

theorem TauCeti.coe_timeDependentFlowMFDerivEquiv_symm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s t : ℝ) (x : M) : ↑(timeDependentFlowMFDerivEquiv hcomplete hn hX s t x).symm = mfderiv% (timeDependentFlowOf X t s) (timeDependentFlowOf X s t x)

The inverse of the linearized time-dependent flow from s to t at x is the differential of the flow from t to s at the flowed point φ_{s,t} x.

@[simp]

theorem TauCeti.timeDependentFlowMFDerivEquiv_symm_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (s t : ℝ) (x : M) (v : TangentSpace I (timeDependentFlowOf X s t x)) : (timeDependentFlowMFDerivEquiv hcomplete hn hX s t x).symm v = (mfderiv% (timeDependentFlowOf X t s) (timeDependentFlowOf X s t x)) v

The inverse of the linearized time-dependent flow applies the differential of the reverse time map at the flowed point.

theorem TauCeti.hasMFDerivAt_timeDependentFlowOf_comp {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {X : ℝ → (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) [FiniteDimensional ℝ E] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {F : Type u_4} {G : Type u_5} {N : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace G] {J : ModelWithCorners ℝ F G} [TopologicalSpace N] [ChartedSpace G N] (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent 1 fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) {τ : N → ℝ} {v : N → M} {z : N} {τ' : TangentSpace J z →L[ℝ] ℝ} {v' : TangentSpace J z →L[ℝ] TangentSpace I (v z)} (hτ : HasMFDerivAt% τ z τ') (hv : HasMFDerivAt% v z v') (s : ℝ) : HasMFDerivAt% (fun (y : N) => timeDependentFlowOf X s (τ y) (v y)) z (mfderiv% (timeDependentFlowOf X s (τ z)) (v z) ∘SL v' + τ'.smulRight (X (τ z) (timeDependentFlowOf X s (τ z) (v z))))

Derivative of a map moved by the time-dependent flow. Let τ : N → ℝ and v : N → M have derivatives τ' and v' at z, and let X be jointly C¹ with complete suspension. The map y ↦ φ_{s, τ y} (v y), with φ_{s, t} = timeDependentFlowOf X s t, has derivative dφ_{s, τ z} ∘ v' + τ' ⊗ X_{τ z} at z: the flow carries the derivative of v, and the varying time adds the velocity of the flow at the moved point.