Documentation

TauCeti.Dynamics.Flow.TimeDependent

Global flows of time-dependent vector fields #

A time-dependent vector field v : ℝ → E → E can be made autonomous on ℝ × E by adjoining the clock equation t' = 1. If this suspended vector field is globally Lipschitz, its global autonomous solution defines the evolution map from an initial time s to a final time t.

This file carries out that construction. The resulting map starts at the prescribed point, solves the original time-dependent equation, is jointly continuous in both times and the initial point, and satisfies the two-time composition law. It is also the unique global solution with a given value at a given time. These properties are the nonautonomous replacement for the group law of an ordinary Flow.

Main declarations #

The construction uses the global autonomous Picard--Lindelöf solution from TauCeti.Analysis.ODE.GlobalSolution.

source
def TauCeti.timeDependentSuspension {E : Type u_1} (v : ℝ → E → E) :
ℝ × E → ℝ × E

The autonomous suspension of a time-dependent vector field: its first component advances the clock at unit speed and its second component is the original field.

Instances For
    source
    @[simp]
    theorem TauCeti.timeDependentSuspension_apply {E : Type u_1} (v : ℝ → E → E) (t : ℝ) (x : E) :
    timeDependentSuspension v (t, x) = (1, v t x)
    source
    noncomputable def TauCeti.timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (s t : ℝ) (x : E) :
    E

    The global time-dependent flow of v. The value timeDependentFlow v hv s t x is the value at time t of the solution which equals x at time s. Global existence follows by applying the autonomous global-solution theorem to the suspended field on ℝ × E.

    Instances For
      source
      theorem TauCeti.globalSolution_timeDependentSuspension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (s t : ℝ) (x : E) :
      ODE.globalSolution (timeDependentSuspension v) hv (s, x) (t - s) = (t, timeDependentFlow v hv s t x)

      The suspended global solution consists of the current time and the time-dependent flow.

      source
      @[simp]
      theorem TauCeti.timeDependentFlow_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (s : ℝ) (x : E) :
      timeDependentFlow v hv s s x = x

      A time-dependent flow starts at its prescribed initial point.

      source
      theorem TauCeti.hasDerivAt_timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (s t : ℝ) (x : E) :
      HasDerivAt (fun (u : ℝ) => timeDependentFlow v hv s u x) (v t (timeDependentFlow v hv s t x)) t

      The time-dependent flow solves the original nonautonomous differential equation.

      source
      @[simp]
      theorem TauCeti.timeDependentFlow_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (r s t : ℝ) (x : E) :
      timeDependentFlow v hv s t (timeDependentFlow v hv r s x) = timeDependentFlow v hv r t x

      Time-dependent evolution through an intermediate time is the same as direct evolution.

      source
      theorem TauCeti.leftInverse_timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (s t : ℝ) :
      Function.LeftInverse (timeDependentFlow v hv t s) (timeDependentFlow v hv s t)

      The evolution from t back to s is a left inverse of the evolution from s to t.

      source
      theorem TauCeti.rightInverse_timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (s t : ℝ) :
      Function.RightInverse (timeDependentFlow v hv t s) (timeDependentFlow v hv s t)

      The evolution from t back to s is a right inverse of the evolution from s to t.

      source
      theorem TauCeti.bijective_timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (s t : ℝ) :
      Function.Bijective (timeDependentFlow v hv s t)

      Each time map of the time-dependent flow is bijective.

      source
      theorem TauCeti.continuous_timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) :
      Continuous fun (p : (ℝ × ℝ) × E) => timeDependentFlow v hv p.1.1 p.1.2 p.2

      The time-dependent flow is jointly continuous in the initial time, final time, and point.

      source
      theorem TauCeti.timeDependentFlow_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K K' : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (hv' : LipschitzWith K' (timeDependentSuspension v)) :
      timeDependentFlow v hv = timeDependentFlow v hv'

      The construction does not depend on the chosen Lipschitz bound for the suspended field.

      source
      theorem TauCeti.timeDependentFlow_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) (s t : ℝ) (x : E) :
      timeDependentFlow v hv s t x = x + ∫ (u : ℝ) in s..t, v u (timeDependentFlow v hv s u x)

      The integral equation of the time-dependent flow: φ(s, t) x = x + ∫ₛᵗ v(u, φ(s, u) x) du.

      source
      theorem TauCeti.eq_timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : ℝ → E → E) {K : NNReal} (hv : LipschitzWith K (timeDependentSuspension v)) {y : ℝ → E} (hy : ∀ (t : ℝ), HasDerivAt y (v t (y t)) t) (s t : ℝ) :
      y t = timeDependentFlow v hv s t (y s)

      Uniqueness of the time-dependent flow. A global solution of y' = v(t, y) is the time-dependent flow through its value at any chosen initial time.