Cross-testing at the L⁴ exponent

The cross-testing identity is restated with space-time L⁴ inputs for the mixed-norm Serrin energy argument. It reuses the Part V regularized identity and the existing cutoff and cross-density limits.

theorem ESS.lps_cross_identity_four {T : ℝ} {a b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pu pv : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsSerrinWeakSolution T a u Du pu) (hV : IsSerrinWeakSolution T b v Dv pv) (hu4 : MeasureTheory.MemLp u (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hv4 : MeasureTheory.MemLp v (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, v (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, b x k * a x k = ((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, u q k * ∑ j : Fin 3, v q j * Dv q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Dv q k j) + ((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, v q k * ∑ j : Fin 3, u q j * Du q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dv q k j * Du q k j)

The cross-testing identity for two finite-energy weak solutions with pressures, when both velocities lie in space-time L⁴.