The flow of a globally Lipschitz vector field

A vector field whose solutions may blow up in finite time generates no flow: the group law φ (t₁ + t₂) = φ t₁ ∘ φ t₂ needs solutions defined for all time. A globally Lipschitz vector field on a Banach space has them, by ODE.globalSolution, and this file assembles them into a Flow ℝ E.

The group law is uniqueness of solutions applied to the time-translated orbit, the identity law is the initial condition, and the joint continuity required by Flow is ODE.continuous_globalSolution.

Main declarations

• TauCeti.flowOfLipschitz: the flow of a globally Lipschitz vector field on a Banach space.
• TauCeti.contDiff_flowOfLipschitz and TauCeti.contDiff_flowOfLipschitz_apply: a globally C^(n+1) field has a C^(n+1) flow, jointly and at each fixed time.
• TauCeti.hasDerivAt_flowOfLipschitz and TauCeti.isIntegralCurve_flowOfLipschitz: its orbits solve the differential equation.
• TauCeti.eq_flowOfLipschitz: every global solution is an orbit of the flow.
• TauCeti.eq_flowOfLipschitz_of_isIntegralCurveOn: the corresponding uniqueness statement for a solution on any time set containing the interval between zero and the chosen time.
• TauCeti.flowOfLipschitz_congr: it does not depend on the chosen Lipschitz bound.
• TauCeti.forall_flowOfLipschitz_eq_self_iff: the rest points of the flow are the zeros of the vector field.

References

• J. Dieudonné, Foundations of Modern Analysis, Academic Press, 1969, Chapter X.

noncomputable def TauCeti.flowOfLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) : Flow ℝ E

The flow of a globally Lipschitz vector field on a Banach space: the time-t map sends an initial point to the value at time t of the unique global solution of γ' = v ∘ γ through it.

Equations

• TauCeti.flowOfLipschitz v hv = { toFun := fun (t : ℝ) (x : E) => ODE.globalSolution v hv x t, cont' := ⋯, map_add' := ⋯, map_zero' := ⋯ }

@[simp]

theorem TauCeti.flowOfLipschitz_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) (t : ℝ) (x : E) : (flowOfLipschitz v hv).toFun t x = ODE.globalSolution v hv x t

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

Independence of the Lipschitz bound. Two Lipschitz witnesses for the same vector field, with possibly different constants, produce the same flow.

theorem TauCeti.contDiff_flowOfLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} (n : ℕ) (v : E → E) (hv : LipschitzWith K v) (hvs : ContDiff ℝ (↑n + 1) v) : ContDiff ℝ (↑n + 1) (Function.uncurry (flowOfLipschitz v hv).toFun)

A globally Lipschitz C^(n+1) vector field has a C^(n+1) global flow, jointly in time and the initial condition.

theorem TauCeti.contDiff_flowOfLipschitz_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} (n : ℕ) (v : E → E) (hv : LipschitzWith K v) (hvs : ContDiff ℝ (↑n + 1) v) (t : ℝ) : ContDiff ℝ (↑n + 1) ((flowOfLipschitz v hv).toFun t)

At each fixed time, the flow of a globally Lipschitz C^(n+1) vector field is C^(n+1) in the initial condition.

theorem TauCeti.hasDerivAt_flowOfLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) (x : E) (t : ℝ) : HasDerivAt (fun (t : ℝ) => (flowOfLipschitz v hv).toFun t x) (v ((flowOfLipschitz v hv).toFun t x)) t

Every orbit of the flow solves the differential equation.

theorem TauCeti.isIntegralCurve_flowOfLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) (x : E) : IsIntegralCurve (fun (t : ℝ) => (flowOfLipschitz v hv).toFun t x) fun (x : ℝ) (y : E) => v y

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

theorem TauCeti.eq_flowOfLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) {γ : ℝ → E} (hγ : ∀ (t : ℝ), HasDerivAt γ (v (γ t)) t) (t : ℝ) : γ t = (flowOfLipschitz v hv).toFun t (γ 0)

Every global solution is an orbit of the flow, namely the one through its initial value.

theorem TauCeti.eq_flowOfLipschitz_of_isIntegralCurveOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) {γ : ℝ → E} {s : Set ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (y : E) => v y) s) {t : ℝ} (hst : Set.uIcc 0 t ⊆ s) : γ t = (flowOfLipschitz v hv).toFun t (γ 0)

Uniqueness on a time set. An integral curve on a set containing the interval between zero and t agrees at t with the globally Lipschitz flow through its value at zero.

theorem TauCeti.forall_flowOfLipschitz_eq_self_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) (x : E) : (∀ (t : ℝ), (flowOfLipschitz v hv).toFun t x = x) ↔ v x = 0

The rest points of the flow are the zeros of the vector field.