Complete vector fields

A vector field is complete when every maximal integral curve is defined for all real time. This file expresses completeness through the joint maximal-flow domain and relates it to the pointwise maximal intervals and to the existence of global integral curves.

Compactly supported C¹ vector fields on boundaryless Banach manifolds are complete. In particular, every C¹ vector field on a compact boundaryless Banach manifold is complete. So is every C¹ vector field admitting a proper map that is constant along its integral curves, such as a Hamiltonian vector field with a proper family of first integrals. These criteria make completeness available without choosing a global flow or assuming finite dimensionality.

Main declarations

• TauCeti.IsCompleteVectorField: the maximal flow is defined at every time and point, with eliminators IsCompleteVectorField.flowDomain_eq_univ, IsCompleteVectorField.mem_flowDomain, and IsCompleteVectorField.mem_maximalIntegralCurveInterval.
• TauCeti.isCompleteVectorField_iff_maximalIntegralCurveInterval: completeness in terms of pointwise maximal intervals.
• TauCeti.isCompleteVectorField_iff_exists_isMIntegralCurve: completeness in terms of global integral curves through every point.
• TauCeti.flowOf_flowOf_neg: for a complete field the time-(-t) map of the maximal flow inverts the time-t map, so (TauCeti.flowOf_surjective) the time-t map is surjective.
• TauCeti.isCompleteVectorField_of_exists_isMIntegralCurveOn: the uniform-time completeness criterion.
• TauCeti.isCompleteVectorField_of_isCompact_of_eq_zero_off: compactly supported fields are complete.
• TauCeti.isCompleteVectorField_of_compactSpace: fields on compact manifolds are complete.
• TauCeti.isCompleteVectorField_of_isProperMap: fields whose maximal integral curves stay in the fibres of a proper map are complete.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 9.16.
• Winston Yin, Mathlib.Geometry.Manifold.IntegralCurve.UniformTime, whose exists_isMIntegralCurve_of_isMIntegralCurveOn supplies the uniform-time criterion.

def TauCeti.IsCompleteVectorField {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] (v : (x : M) → TangentSpace I x) : Prop

A vector field is complete when its maximal flow is defined at every time and point.

theorem TauCeti.IsCompleteVectorField.flowDomain_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] {v : (x : M) → TangentSpace I x} (hv : IsCompleteVectorField v) : flowDomain v = Set.univ

The maximal-flow domain of a complete vector field is all of ℝ × M. This is the defining property, named so that it can be used for rewriting.

theorem TauCeti.IsCompleteVectorField.mem_flowDomain {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] {v : (x : M) → TangentSpace I x} (hv : IsCompleteVectorField v) (t : ℝ) (x : M) : (t, x) ∈ flowDomain v

Every time and point lie in the maximal-flow domain of a complete vector field.

theorem TauCeti.IsCompleteVectorField.mem_maximalIntegralCurveInterval {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] {v : (x : M) → TangentSpace I x} (hv : IsCompleteVectorField v) (x : M) (t : ℝ) : t ∈ maximalIntegralCurveInterval v x

Every time lies in each maximal interval of a complete vector field.

theorem TauCeti.isCompleteVectorField_iff_maximalIntegralCurveInterval {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] {v : (x : M) → TangentSpace I x} : IsCompleteVectorField v ↔ ∀ (x : M), maximalIntegralCurveInterval v x = Set.univ

A vector field is complete precisely when every pointwise maximal interval is all of ℝ.

theorem TauCeti.IsCompleteVectorField.maximalIntegralCurveInterval_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] {v : (x : M) → TangentSpace I x} (hv : IsCompleteVectorField v) (x : M) : maximalIntegralCurveInterval v x = Set.univ

Every pointwise maximal interval of a complete vector field is all of ℝ.

theorem TauCeti.isCompleteVectorField_iff_exists_isMIntegralCurve {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] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) : IsCompleteVectorField v ↔ ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v

A C¹ vector field is complete precisely when a global integral curve through every point exists.

theorem TauCeti.isCompleteVectorField_of_exists_isMIntegralCurveOn {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] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) {ε : ℝ} (hε : 0 < ε) (h : ∀ (x : M), ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurveOn γ v (Set.Ioo (-ε) ε)) : IsCompleteVectorField v

A uniform positive time of existence for local integral curves through every point makes a C¹ vector field complete.

theorem TauCeti.IsCompleteVectorField.exists_isMIntegralCurve {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] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField v) (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) (x : M) : ∃ (γ : ℝ → M), γ 0 = x ∧ IsMIntegralCurve γ v

A global integral curve of a complete C¹ vector field through a prescribed point.

theorem TauCeti.flowOf_flowOf_neg {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] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) (t : ℝ) (x : M) : flowOf v t (flowOf v (-t) x) = x

For a complete C¹ vector field, the time-(-t) map of the maximal flow inverts the time-t map.

theorem TauCeti.flowOf_surjective {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] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) (t : ℝ) : Function.Surjective (flowOf v t)

For a complete C¹ vector field, the time-t map of the maximal flow is surjective.

theorem TauCeti.isCompleteVectorField_of_isCompact_of_eq_zero_off {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] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] [CompleteSpace E] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) {K : Set M} (hK : IsCompact K) (hvK : ∀ x ∉ K, v x = 0) : IsCompleteVectorField v

A C¹ vector field that vanishes outside a compact set is complete.

theorem TauCeti.isCompleteVectorField_of_compactSpace {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] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] [CompleteSpace E] [CompactSpace M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) : IsCompleteVectorField v

Every C¹ vector field on a compact boundaryless Banach manifold is complete.

theorem TauCeti.isCompleteVectorField_of_isProperMap {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] [T2Space M] [BoundarylessManifold I M] [IsManifold I 1 M] [CompleteSpace E] {Y : Type u_4} [TopologicalSpace Y] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (x : M) => ⟨x, v x⟩) {G : M → Y} (hG : IsProperMap G) (hGv : ∀ (x : M), ∀ t ∈ maximalIntegralCurveInterval v x, G (maximalIntegralCurve v x t) = G x) : IsCompleteVectorField v

A C¹ vector field with a proper invariant map is complete. If a proper map G is constant along every maximal integral curve of v, then each maximal integral curve stays in the compact fibre of G through its initial point, so it is defined for all time. No regularity of the fibres is needed.