The variational equation of a flow

Let v be a globally Lipschitz, continuously differentiable vector field on a Banach space and φ its flow (TauCeti.flowOfLipschitz). The derivative Dφₜ(x) of the time-t map at x describes how a perturbation of the initial condition x evolves along the orbit of x. It is the solution of the linear equation

Dφₜ(x) = id + ∫₀ᵗ Dv(φ_τ x) ∘ Dφ_τ(x) dτ,

equivalently d/dt Dφₜ(x) = Dv(φₜ x) ∘ Dφₜ(x), with Dφ₀(x) = id. This is the equation used to compute the first-order dependence of the flow on parameters of the vector field.

Main results

• TauCeti.differentiable_flowOfLipschitz_apply: the time-t map is differentiable.
• TauCeti.fderiv_flowOfLipschitz_eq_id_add_integral: the integral form.
• TauCeti.hasDerivAt_fderiv_flowOfLipschitz: the differential form.
• TauCeti.hasDerivAt_fderiv_flowOfLipschitz_apply: the differential form applied to a vector.
• Flow.fderiv_add, Flow.fderiv_neg_comp, Flow.fderiv_comp_neg, Flow.fderivUnit, Flow.ringInverse_fderiv: for a flow whose time maps are differentiable at the relevant points, Dϕ_{s+t}(x) = Dϕ_s(ϕ_t x) ∘ Dϕ_t(x), and Dϕ_t(x) is invertible with inverse Dϕ_{-t}(ϕ_t x).
• Flow.fderiv_apply_of_hasDerivAt: the derivative of a flow carries its velocity field along.
• TauCeti.continuous_fderiv_flowOfLipschitz, TauCeti.continuous_fderiv_flowOfLipschitz_neg: for a C¹ field, τ ↦ Dφ_τ(x) and its inverse σ ↦ Dφ_{-σ}(φ_σ x) are continuous.
• TauCeti.contDiff_timeDependentFlow and TauCeti.hasDerivAt_fderiv_timeDependentFlow: the time-dependent flow φ(s, t) of a jointly C^(n+1) field (TauCeti.timeDependentFlow) is C^(n+1) in (s, t, x), and ∂ₜ Dφ(s, t)(x) = Dvₜ(φ(s, t) x) ∘ Dφ(s, t)(x).
• TauCeti.differentiable_timeDependentFlow and TauCeti.fderiv_timeDependentFlow_eq_dysonSeriesLeft: consequently Dφ(s, t)(x) exists and is the propagator TauCeti.dysonSeriesLeft of the linearized equation ξ' = Dv_r(φ(s, r) x) ξ along the orbit of x, from time s to time t.

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

The time-t map of the flow of a Lipschitz C¹ vector field is differentiable.

theorem TauCeti.continuous_fderiv_flowOfLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) (hvs : ContDiff ℝ 1 v) (x : E) : Continuous fun (τ : ℝ) => fderiv ℝ ((flowOfLipschitz v hv).toFun τ) x

The derivative of the time-τ map at a fixed point is continuous in τ.

theorem TauCeti.fderiv_flowOfLipschitz_eq_id_add_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) (hvs : ContDiff ℝ 1 v) (x : E) (t : ℝ) : fderiv ℝ ((flowOfLipschitz v hv).toFun t) x = ContinuousLinearMap.id ℝ E + ∫ (τ : ℝ) in 0..t, fderiv ℝ v ((flowOfLipschitz v hv).toFun τ x) ∘SL fderiv ℝ ((flowOfLipschitz v hv).toFun τ) x

The variational equation, integral form. For a globally Lipschitz C¹ vector field, the derivative of the time-t map of its flow at x is id + ∫₀ᵗ Dv(φ_τ x) ∘ Dφ_τ(x) dτ.

theorem TauCeti.hasDerivAt_fderiv_flowOfLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) (hvs : ContDiff ℝ 1 v) (x : E) (t : ℝ) : HasDerivAt (fun (τ : ℝ) => fderiv ℝ ((flowOfLipschitz v hv).toFun τ) x) (fderiv ℝ v ((flowOfLipschitz v hv).toFun t x) ∘SL fderiv ℝ ((flowOfLipschitz v hv).toFun t) x) t

The variational equation, differential form. For a globally Lipschitz C¹ vector field, t ↦ Dφₜ(x) is differentiable with derivative Dv(φₜ x) ∘ Dφₜ(x).

theorem TauCeti.hasDerivAt_fderiv_flowOfLipschitz_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) (hvs : ContDiff ℝ 1 v) (x w : E) (t : ℝ) : HasDerivAt (fun (τ : ℝ) => (fderiv ℝ ((flowOfLipschitz v hv).toFun τ) x) w) ((fderiv ℝ v ((flowOfLipschitz v hv).toFun t x)) ((fderiv ℝ ((flowOfLipschitz v hv).toFun t) x) w)) t

The variational equation applied to a vector: the derivative of the orbit of the variation Dφₜ(x) w is Dv(φₜ x) (Dφₜ(x) w).

theorem Flow.fderiv_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {s t : ℝ} {x : E} (hs : DifferentiableAt ℝ (ϕ.toFun s) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : fderiv ℝ (ϕ.toFun (s + t)) x = fderiv ℝ (ϕ.toFun s) (ϕ.toFun t x) ∘SL fderiv ℝ (ϕ.toFun t) x

The chain rule for the group law of a flow: Dϕ_{s+t}(x) = Dϕ_s(ϕ_t x) ∘ Dϕ_t(x).

@[simp]

theorem Flow.fderiv_neg_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {t : ℝ} {x : E} (hs : DifferentiableAt ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : fderiv ℝ (ϕ.toFun (-t)) (ϕ.toFun t x) ∘SL fderiv ℝ (ϕ.toFun t) x = ContinuousLinearMap.id ℝ E

The derivative of the time-(-t) map at ϕ t x is a left inverse of Dϕ_t(x).

@[simp]

theorem Flow.fderiv_comp_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {t : ℝ} {x : E} (hs : DifferentiableAt ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : fderiv ℝ (ϕ.toFun t) x ∘SL fderiv ℝ (ϕ.toFun (-t)) (ϕ.toFun t x) = ContinuousLinearMap.id ℝ E

The derivative of the time-(-t) map at ϕ t x is a right inverse of Dϕ_t(x).

theorem Flow.isInvertible_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {t : ℝ} {x : E} (ϕ : Flow ℝ E) (hs : DifferentiableAt ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : (fderiv ℝ (ϕ.toFun t) x).IsInvertible

The derivative of a differentiable time map is invertible when the reverse time map is differentiable at the image point. No completeness of the model space is needed.

noncomputable def Flow.fderivUnit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {t : ℝ} {x : E} (hs : DifferentiableAt ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : (E →L[ℝ] E)ˣ

The derivative of a flow as a unit. When the time-t map is differentiable at x and the time-(-t) map at ϕ t x, the derivative Dϕ_t(x) is invertible, with inverse Dϕ_{-t}(ϕ_t x).

@[simp]

theorem Flow.coe_fderivUnit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {t : ℝ} {x : E} (hs : DifferentiableAt ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : ↑(fderivUnit hs ht) = fderiv ℝ (ϕ.toFun t) x

The unit fderivUnit is the derivative Dϕ_t(x).

@[simp]

theorem Flow.coe_inv_fderivUnit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {t : ℝ} {x : E} (hs : DifferentiableAt ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : ↑(fderivUnit hs ht)⁻¹ = fderiv ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)

The inverse of the unit fderivUnit is the derivative Dϕ_{-t}(ϕ_t x) of the reverse time map.

@[simp]

theorem Flow.ringInverse_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {t : ℝ} {x : E} (hs : DifferentiableAt ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : Ring.inverse (fderiv ℝ (ϕ.toFun t) x) = fderiv ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)

The inverse of the derivative of a flow is the derivative of the reverse time map.

theorem Flow.fderiv_apply_of_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {t : ℝ} {x a b : E} (hx : HasDerivAt (fun (s : ℝ) => ϕ.toFun s x) a 0) (hy : HasDerivAt (fun (s : ℝ) => ϕ.toFun s (ϕ.toFun t x)) b 0) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : (fderiv ℝ (ϕ.toFun t) x) a = b

The derivative of a flow carries its velocity field along: if the orbits of x and of ϕ t x have velocities a and b at time 0, then Dϕ_t(x) a = b.

theorem TauCeti.continuous_fderiv_flowOfLipschitz_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {v : E → E} {K : NNReal} (hv : LipschitzWith K v) (hvs : ContDiff ℝ 1 v) (x : E) : Continuous fun (σ : ℝ) => fderiv ℝ ((flowOfLipschitz v hv).toFun (-σ)) ((flowOfLipschitz v hv).toFun σ x)

The inverse derivative along an orbit is continuous: for a globally Lipschitz C¹ field, σ ↦ Dφ_{-σ}(φ_σ x), the inverse of Dφ_σ(x), is continuous.

Time-dependent flows

The time-dependent flow is the space component of the flow of the suspended autonomous field (t, x) ↦ (1, v t x), so its smoothness and its variational equation follow from those of autonomous flows.

theorem TauCeti.contDiff_timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} {v : ℝ → E → E} (hv : LipschitzWith K (timeDependentSuspension v)) (n : ℕ) (hvs : ContDiff ℝ (↑n + 1) fun (p : ℝ × E) => v p.1 p.2) : ContDiff ℝ (↑n + 1) fun (p : (ℝ × ℝ) × E) => timeDependentFlow v hv p.1.1 p.1.2 p.2

A time-dependent field which is jointly C^(n+1) has a C^(n+1) time-dependent flow, jointly in the initial time, the final time and the initial point.

theorem TauCeti.hasDerivAt_fderiv_timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} {v : ℝ → E → E} (hv : LipschitzWith K (timeDependentSuspension v)) (hvs : ContDiff ℝ 1 fun (p : ℝ × E) => v p.1 p.2) (s t : ℝ) (x : E) : HasDerivAt (fun (u : ℝ) => fderiv ℝ (timeDependentFlow v hv s u) x) (fderiv ℝ (v t) (timeDependentFlow v hv s t x) ∘SL fderiv ℝ (timeDependentFlow v hv s t) x) t

The variational equation of a time-dependent flow. For a jointly C¹ time-dependent field whose suspension is globally Lipschitz, u ↦ Dφ(s, u)(x) is differentiable with derivative D(v t)(φ(s, t) x) ∘ Dφ(s, t)(x) at t.

theorem TauCeti.differentiable_timeDependentFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} {v : ℝ → E → E} (hv : LipschitzWith K (timeDependentSuspension v)) (hvs : ContDiff ℝ 1 fun (p : ℝ × E) => v p.1 p.2) (s t : ℝ) : Differentiable ℝ (timeDependentFlow v hv s t)

Each time map of the time-dependent flow of a jointly C¹ field is differentiable.

theorem TauCeti.fderiv_timeDependentFlow_eq_dysonSeriesLeft {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} {v : ℝ → E → E} (hv : LipschitzWith K (timeDependentSuspension v)) (hvs : ContDiff ℝ 1 fun (p : ℝ × E) => v p.1 p.2) (s t : ℝ) (x : E) : fderiv ℝ (timeDependentFlow v hv s t) x = dysonSeriesLeft (fun (r : ℝ) => fderiv ℝ (v (s + r)) (timeDependentFlow v hv s (s + r) x)) (t - s)

The derivative of a time-dependent flow is the propagator of the linearized equation. For a jointly C¹ time-dependent field whose suspension is globally Lipschitz, the derivative Dφ(s, t)(x) of the evolution from time s to time t is the propagator from 0 to t - s of the linear equation ξ' = M r ξ with M r = Dv_{s + r}(φ(s, s + r) x), the linearization of the field along the orbit of x.