Energy identities for absolutely continuous curves

The chain rule is separated from the ODE existence construction. It applies to any absolutely-continuous curve in a real inner-product space and can therefore be reused for linear equations with measurable coefficients.

theorem AbsolutelyContinuousOnInterval.norm_sq {E : Type u_1} [NormedAddCommGroup E] {y : ℝ → E} {a b : ℝ} (hy : AbsolutelyContinuousOnInterval y a b) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => ‖y t‖ ^ 2) a b

Squaring the norm preserves absolute continuity on a compact interval.

theorem HasDerivAt.norm_sq_inner {E : Type u_1} [NormedAddCommGroup E] {y : ℝ → E} {y' : E} {t : ℝ} [InnerProductSpace ℝ E] (hy : HasDerivAt y y' t) : HasDerivAt (fun (s : ℝ) => ‖y s‖ ^ 2) (2 * Inner.inner ℝ (y t) y') t

The norm-square chain rule at every differentiability point.

theorem AVenhance.Infra.ODE.integral_energy_eq_norm_sq_sub {E : Type u_1} [NormedAddCommGroup E] {y q : ℝ → E} {a b : ℝ} [InnerProductSpace ℝ E] (hy : AbsolutelyContinuousOnInterval (fun (t : ℝ) => ‖y t‖ ^ 2) a b) (hq : ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → HasDerivAt (fun (s : ℝ) => ‖y s‖ ^ 2) (2 * inner ℝ (y t) (q t)) t) : ∫ (t : ℝ) in a..b, 2 * inner ℝ (y t) (q t) = ‖y b‖ ^ 2 - ‖y a‖ ^ 2

Integral energy identity from the a.e. chain-rule derivative.

theorem AVenhance.Infra.ODE.IsLinearIntegralSolution.energy_identity {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace ℝ E] {A : ℝ → E →L[ℝ] E} {f y : ℝ → E} {y₀ : E} {a b : ℝ} (hab : a ≤ b) (hy : IsLinearIntegralSolution A f y₀ a b y) (h_rhs : IntervalIntegrable (linearRhs A f y) MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, 2 * inner ℝ (y t) ((A t) (y t) + f t) = ‖y b‖ ^ 2 - ‖y a‖ ^ 2

The integral energy formula for an absolutely-continuous solution with an a.e. derivative.

theorem AVenhance.Infra.ODE.LinearODEData.IsSolution.energy_absolutelyContinuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) (hu : D.IsSolution u) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => ‖extendCurve hab u t‖ ^ 2) a b

The squared norm of the constructed solution is absolutely continuous.

theorem AVenhance.Infra.ODE.LinearODEData.IsSolution.ae_energy_deriv {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace ℝ E] {a b : ℝ} {hab : a ≤ b} (D : LinearODEData a b hab) (u : C(↑(Set.Icc a b), E)) (hu : D.IsSolution u) : ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → HasDerivAt (fun (s : ℝ) => ‖extendCurve hab u s‖ ^ 2) (2 * inner ℝ (extendCurve hab u t) ((D.A t) (extendCurve hab u t) + D.f t)) t

A constructed solution satisfies the norm-square chain rule almost everywhere.