The flow law for maximal integral curves

The maximal integral curve of an autonomous vector field can be restarted at any time in its interval of existence. Its new maximal interval is the translate of the original interval, and the restarted curve is the corresponding translate of the original curve. These are the domain and value laws that turn the family maximalIntegralCurve v into a partial flow.

The domain statement is essential: maximalIntegralCurve is total only by assigning its initial point as a junk value outside the interval of existence, so an unconditional flow equation would be false. The results below always carry the precise membership hypotheses.

Main results

• mem_maximalIntegralCurveInterval_maximalIntegralCurve_iff: the maximal interval after restarting at t is exactly the translate by -t of the original interval.
• maximalIntegralCurve_add: the domain-aware flow law φ x (t + s) = φ (φ x t) s.
• maximalIntegralCurveFlowDomain: the natural domain of the maximal flow, which is everything for a complete field (maximalIntegralCurveFlowDomain_eq_univ).
• isOpen_maximalIntegralCurveFlowDomain: the natural domain is open.
• contMDiffOn_maximalIntegralCurve: the maximal flow of a C^n vector field (1 ≤ n ≤ ∞) is C^n on its natural domain, and continuousAt_maximalIntegralCurve records its joint continuity at each point of that domain.
• mapClusterPt_atTop_maximalIntegralCurve: the ω-limit set of a maximal integral curve defined for all positive time is invariant under the maximal flow.

References

• [Lee, J. M. (2012). Introduction to Smooth Manifolds. Springer New York.][lee2012], Chapter 9, especially Theorem 9.12.

theorem TauCeti.maximalIntegralCurve_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {s t : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (ht : t ∈ maximalIntegralCurveInterval v x) (hts : t + s ∈ maximalIntegralCurveInterval v x) : maximalIntegralCurve v x (t + s) = maximalIntegralCurve v (maximalIntegralCurve v x t) s

The flow law for the maximal integral curve. If both t and t + s lie in the maximal interval through x, restarting the curve at time t and running it for time s gives its value at time t + s.

@[simp]

theorem TauCeti.mem_maximalIntegralCurveInterval_maximalIntegralCurve_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {s t : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (ht : t ∈ maximalIntegralCurveInterval v x) : s ∈ maximalIntegralCurveInterval v (maximalIntegralCurve v x t) ↔ t + s ∈ maximalIntegralCurveInterval v x

Restarting a maximal integral curve at time t translates its maximal interval by -t. This characterizes the domain of the partial flow without reference to the chosen integral-curve witnesses.

theorem TauCeti.maximalIntegralCurveInterval_maximalIntegralCurve_eq_preimage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {t : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (ht : t ∈ maximalIntegralCurveInterval v x) : maximalIntegralCurveInterval v (maximalIntegralCurve v x t) = (fun (s : ℝ) => t + s) ⁻¹' maximalIntegralCurveInterval v x

Set form of mem_maximalIntegralCurveInterval_maximalIntegralCurve_iff: the maximal interval after restarting at t is the preimage of the original interval under translation by t.

The domain and regularity of the maximal flow

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

The natural domain of the maximal flow of v, consisting of the pairs (x, t) for which the maximal integral curve through x is defined at time t.

@[simp]

theorem TauCeti.mem_maximalIntegralCurveFlowDomain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {p : M × ℝ} : p ∈ maximalIntegralCurveFlowDomain v ↔ p.2 ∈ maximalIntegralCurveInterval v p.1

Membership in the natural domain of the maximal flow.

theorem TauCeti.maximalIntegralCurveFlowDomain_eq_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} (h : ∀ (x : M), maximalIntegralCurveInterval v x = Set.univ) : maximalIntegralCurveFlowDomain v = Set.univ

For a complete vector field, whose maximal integral curves are all defined for all time, the natural domain of the maximal flow is everything.

theorem TauCeti.isOpen_maximalIntegralCurveFlowDomain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) : IsOpen (maximalIntegralCurveFlowDomain v)

The natural domain of the maximal flow is open. This is openness jointly in the initial point and time, not merely openness of each individual maximal interval.

theorem TauCeti.contMDiffOn_maximalIntegralCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) : ContMDiffOn (I.prod (modelWithCornersSelf ℝ ℝ)) I (↑n) (fun (p : M × ℝ) => maximalIntegralCurve v p.1 p.2) (maximalIntegralCurveFlowDomain v)

Smoothness of the maximal flow. The maximal flow of a C^n vector field, 1 ≤ n ≤ ∞, on a boundaryless manifold modelled on a complete normed space is jointly C^n in its initial point and time on its natural domain.

theorem TauCeti.continuousAt_maximalIntegralCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) {p : M × ℝ} (hp : p.2 ∈ maximalIntegralCurveInterval v p.1) : ContinuousAt (fun (q : M × ℝ) => maximalIntegralCurve v q.1 q.2) p

Continuity of the maximal flow. The maximal flow of a C^1 vector field on a boundaryless manifold modelled on a complete normed space is jointly continuous in its initial point and time at every point of its natural domain.

theorem TauCeti.mapClusterPt_atTop_maximalIntegralCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {s : ℝ} {x : M} [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] [CompleteSpace E] (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hx : Set.Ici 0 ⊆ maximalIntegralCurveInterval v x) {z : M} (hz : MapClusterPt z Filter.atTop (maximalIntegralCurve v x)) (hs : s ∈ maximalIntegralCurveInterval v z) : MapClusterPt (maximalIntegralCurve v z s) Filter.atTop (maximalIntegralCurve v x)

The ω-limit set of a forward maximal integral curve is invariant under the maximal flow. If the maximal integral curve through x is defined for all positive time and z is one of its cluster points as t → ∞, then so is every point of the maximal integral curve through z.