The energy identity for a linear Stokes-type system

Let v be a weak solution of ∂ₜv - Δv + div H + ∇q = 0 on ℝ³ × (c, d), tested against smooth compactly supported vector fields, with div v = 0 and v, its first and second spatial derivatives, ∂ₜv, H and q square integrable. The kinetic energy E(t) = ∫ |v(x, t)|² dx has weak derivative -2 ∫ |∇v|² + 2 ∫ H : ∇v; if moreover t ↦ v(·, t) is continuous into L² on [c, d], the energy identity holds between any two times of [c, d] (prop:lps-smoothing). No regularity of q or H beyond square integrability is used.

theorem ESS.lps_energy_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} {H : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → ℝ} {q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (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)))) (hDv : MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))) (hD2v : MeasureTheory.MemLp D2v 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)))) (hH : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => H z i j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))) (hq : MeasureTheory.MemLp q 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))) (hdiv : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)), ∑ i : Fin 3, Dv z i i = 0) (heq : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo c d), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo c d), ∑ i : Fin 3, Dtv z i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, H z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Dv z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - q z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) : 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, ∑ j : Fin 3, Dv (x, t) i j ^ 2) + 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, H (x, t) i j * Dv (x, t) i j

The weak energy identity: for a weak solution of ∂ₜv - Δv + div H + ∇q = 0 on ℝ³ × (c, d) with div v = 0, the kinetic energy ∫ |v(x, t)|² dx has weak time derivative -2 ∫ |∇v|² + 2 ∫ H : ∇v on (c, d) (prop:lps-smoothing).

theorem ESS.lps_energy_eq_intervalIntegral {c d : ℝ} (hcd : 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} {H : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → ℝ} {q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (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)))) (hDv : MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))) (hD2v : MeasureTheory.MemLp D2v 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)))) (hH : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => H z i j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))) (hq : MeasureTheory.MemLp q 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)))) (hdiv : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo c d)), ∑ i : Fin 3, Dv z i i = 0) (heq : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo c d), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo c d), ∑ i : Fin 3, Dtv z i * φ z i - ∑ i : Fin 3, ∑ j : Fin 3, H z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Dv z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - q z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0) (hslice : ∀ t ∈ Set.Icc c d, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => v (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc c d, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => v (x, s) - v (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc c d)) (nhds 0)) (s t : ℝ) : c ≤ s → s ≤ t → t ≤ d → (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, v (x, t) i ^ 2) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, v (x, s) i ^ 2 = ∫ (τ : ℝ) in s..t, (-2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Dv (x, τ) i j ^ 2) + 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, H (x, τ) i j * Dv (x, τ) i j

The energy identity between any two times: if moreover every slice v(·, t), t ∈ [c, d], is square integrable and t ↦ v(·, t) is continuous into L² on [c, d], then E(t) - E(s) = ∫ₛᵗ (-2 ∫ |∇v|² + 2 ∫ H : ∇v) for c ≤ s ≤ t ≤ d (prop:lps-smoothing).