Documentation

TauCeti.Geometry.Manifold.IntegralCurve.GlobalFlow

The flow of a complete vector field #

A C¹ vector field v on a boundaryless manifold is complete when its maximal integral curves are all defined for all time. Its maximal integral curves then assemble into a flow of ℝ on the manifold, and this file packages them as a Mathlib Flow. Every C¹ vector field on a compact boundaryless manifold is complete (isCompleteVectorField_of_compactSpace).

Main declarations #

References #

source
noncomputable def TauCeti.globalFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] (v : (x : M) → TangentSpace I x) (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) :
Flow ℝ M

The flow of a complete C¹ vector field: globalFlow v hv hcomplete t x is the value at time t of the integral curve of v through x.

Instances For
    source
    @[simp]
    theorem TauCeti.globalFlow_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I 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) :
    (globalFlow v hv hcomplete).toFun t x = maximalIntegralCurve v x t

    The flow at time t is the maximal integral curve at time t.

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

    For a complete C¹ vector field, the maximal flow flowOf v is the global flow.

    source
    theorem TauCeti.isMIntegralCurve_globalFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) (x : M) :
    IsMIntegralCurve (fun (t : ℝ) => (globalFlow v hv hcomplete).toFun t x) v

    The orbits of the flow are integral curves of the field.

    source
    theorem TauCeti.apply_globalFlow_eq_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) {f : M → ℝ} {a b : ℝ} (hf : Continuous f) {U : Set M} (hU : IsOpen U) (hvU : ∀ y ∈ U, (d% f y) (v y) = -1) (hband : ∀ (y : M), a ≤ f y → f y ≤ b → y ∈ U) {x : M} {t : ℝ} (ht : 0 ≤ t) (hxt : a ≤ f x - t) (hxb : f x ≤ b) :
    f ((globalFlow v hv hcomplete).toFun t x) = f x - t

    Unit-speed descent along a flow. Let v be a complete C¹ vector field with df(v) = -1 on an open set U containing the band a ≤ f ≤ b. If f x ≤ b, then f decreases at unit speed along the flow line of x until it reaches the level a.

    source
    theorem TauCeti.mvfderiv_apply_eq_one_of_eventually_apply_globalFlow_eq_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) {f : M → ℝ} {x : M} (hf : MDiffAt f x) (hfx : ∀ᶠ (t : ℝ) in nhds 0, f ((globalFlow v hv hcomplete).toFun t x) = f x + t) :
    (d% f x) (v x) = 1

    A function translated by a flow has unit derivative along the field. If f is differentiable at x and f (ψ_t x) = f x + t for all times t near 0, where ψ is the flow of v, then df_x(v x) = 1.

    source
    theorem TauCeti.isRegularValue_of_apply_globalFlow_eq_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) {f : M → ℝ} {a b : ℝ} (hf : ∀ (x : M), f x ∈ Set.Ioo a b → MDiffAt f x) (hfv : ∀ (x : M) (t : ℝ), f x ∈ Set.Ioo a b → f x + t ∈ Set.Ioo a b → f ((globalFlow v hv hcomplete).toFun t x) = f x + t) {c : ℝ} (hc : c ∈ Set.Ioo a b) :
    IsRegularValue I (modelWithCornersSelf ℝ ℝ) f c

    Values swept by a flow are regular. If f is differentiable on the band a < f < b and the flow ψ of v translates f at unit speed there, f (ψ_t x) = f x + t whenever f x and f x + t lie in (a, b), then every value in (a, b) is a regular value of f.

    source
    theorem TauCeti.globalFlow_eq_of_isMIntegralCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) {γ : ℝ → M} (hγ : IsMIntegralCurve γ v) (t : ℝ) :
    (globalFlow v hv hcomplete).toFun t (γ 0) = γ t

    Every integral curve of the field is an orbit of the flow.

    source
    theorem TauCeti.forall_globalFlow_eq_self_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hv : ContMDiff I I.tangent 1 fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) (x : M) :
    (∀ (t : ℝ), (globalFlow v hv hcomplete).toFun t x = x) ↔ v x = 0

    A point is stationary under the complete flow exactly when the vector field vanishes there.

    This is not a simp lemma: globalFlow_apply already rewrites flow evaluations to the maximal integral curve.

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

    The flow of a complete C^n vector field, 1 ≤ n, is jointly C^n in time and space.

    source
    theorem TauCeti.contMDiff_globalFlow_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField v) {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hvn : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (t : ℝ) :
    ContMDiff I I (↑n) ((globalFlow v ⋯ hcomplete).toFun t)

    For a fixed time t, the time-t map of the flow of a complete C^n vector field, 1 ≤ n, is C^n.

    source
    theorem TauCeti.mfderiv_globalFlow_apply_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I 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) :
    (mfderiv% ((globalFlow v hv hcomplete).toFun t) x) (v x) = v ((globalFlow v hv hcomplete).toFun t x)

    The flow preserves its generating field. The differential of the time-t map of the flow of a complete C¹ vector field v carries v at x to v at the image of x.

    source
    noncomputable def TauCeti.globalFlowDiffeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField v) {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hvn : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (t : ℝ) :
    Diffeomorph I I M M ↑n

    The time-t map of the flow of a complete C^n vector field, 1 ≤ n, as a C^n diffeomorphism. Its inverse is the time-(-t) map.

    Instances For
      source
      @[simp]
      theorem TauCeti.globalFlowDiffeomorph_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField v) {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hvn : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (t : ℝ) (x : M) :
      (globalFlowDiffeomorph hcomplete hn hvn t) x = (globalFlow v ⋯ hcomplete).toFun t x

      The diffeomorphism globalFlowDiffeomorph is the time-t map of the flow.

      source
      theorem TauCeti.coe_globalFlowDiffeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField v) {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hvn : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (t : ℝ) :
      ⇑(globalFlowDiffeomorph hcomplete hn hvn t) = (globalFlow v ⋯ hcomplete).toFun t

      As a function, globalFlowDiffeomorph is the time-t map of the flow.

      source
      @[simp]
      theorem TauCeti.globalFlowDiffeomorph_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField v) {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hvn : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (t : ℝ) (x : M) :
      (globalFlowDiffeomorph hcomplete hn hvn t).symm x = (globalFlow v ⋯ hcomplete).toFun (-t) x

      The inverse of globalFlowDiffeomorph at time t is the time-(-t) map of the flow.

      source
      noncomputable def TauCeti.globalFlowDiffeomorphHom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField v) {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hvn : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) :
      ℝ →+ Additive (Diffeomorph I I M M ↑n)

      The flow of a complete C^n vector field, 1 ≤ n, as a homomorphism from the additive group of times to the group of C^n self-diffeomorphisms, written additively as for AddAction.toPermHom: time s + t acts as time s after time t.

      Instances For
        source
        @[simp]
        theorem TauCeti.toMul_globalFlowDiffeomorphHom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 1 M] [BoundarylessManifold I M] {v : (x : M) → TangentSpace I x} (hcomplete : IsCompleteVectorField v) {n : ℕ∞} (hn : 1 ≤ n) [IsManifold I (↑n) M] (hvn : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (t : ℝ) :
        Additive.toMul ((globalFlowDiffeomorphHom hcomplete hn hvn) t) = globalFlowDiffeomorph hcomplete hn hvn t

        The image of a time under globalFlowDiffeomorphHom is the time-t diffeomorphism.