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.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.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.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.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.