Ordered Sobolev energy time chain

Differentiable L² trajectories for the finitely many ordered derivatives produce the exact time derivative of the H^m energy.

theorem ESS.lps_ordered_energy_time_chain (m : ℕ) (u q : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hu : ∀ (s : ℝ) (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) i) 2 MeasureTheory.volume) (hq : ∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => q (x, t) i) 2 MeasureTheory.volume) (hcurve : ∀ (i : Fin 3), ∀ α ∈ CKN.sobolevWords m, HasDerivAt (fun (s : ℝ) => MeasureTheory.MemLp.toLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) i) ⋯) (MeasureTheory.MemLp.toLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => q (x, t) i) ⋯) t) : HasDerivAt (fun (s : ℝ) => ∑ i : Fin 3, ∑ α ∈ CKN.sobolevWords m, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, s) i) x ^ 2) (2 * ∑ i : Fin 3, ∑ α ∈ CKN.sobolevWords m, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x * CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => q (y, t) i) x) t

Differentiable L² curves of every ordered derivative imply the time-chain identity in eq:lps-regularized-Hm-identity.