The time derivative of the kinetic energy on a whole-space slab

For a field with square-integrable space-time weak derivatives on ℝ³ × (c, d), the kinetic energy t ↦ ∫ |v(x, t)|² dx has the weak time derivative 2 ∫ v · ∂ₜv dx on (c, d) (prop:lps-smoothing). The localized time identity for |v|² is tested against χ(t) ζₙ(x) with spatial cutoffs ζₙ increasing to one, and the cutoffs are removed by dominated convergence.

theorem ESS.lps_kineticEnergy_hasWeakDerivOn {c d : ℝ} {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hderiv : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo c d) v Dv D2v Dtv) (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))) (hDtv : MeasureTheory.MemLp Dtv 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))) : CKN.HasWeakDerivOn (Set.Ioo c d) (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, v (x, t) i ^ 2) fun (t : ℝ) => 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, v (x, t) i * Dtv (x, t) i

The kinetic energy of a field with square-integrable space-time weak derivatives on ℝ³ × (c, d) has weak time derivative 2 ∫ v · ∂ₜv dx on (c, d) (prop:lps-smoothing).