Energy equality under the mixed-norm Serrin condition

The zero-start identity is obtained from the mollified cross-testing argument when the velocity belongs to space-time L⁴.

theorem ESS.lps_serrin_energy_equality {T : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hLH : CKN.IsLerayHopfSolution T a u Du) (hSerrin : (∃ (s : ℝ), 3 < s ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤) ∨ ∫⁻ (t : ℝ) in Set.Ioo 0 T, essSup (fun (x : CKN.Foundation.Parabolic.Vec3) => ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)))) MeasureTheory.volume ^ 2 < ⊤) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k = -2 * ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Du q k j

Energy equality from the initial time for almost every positive time under either Serrin condition in thm:lps (lem:lps-energy-equality).