Finite Serrin cross-density limits

The energy interpolation and the Serrin mixed norm provide the two oriented convection pairings needed for the finite-exponent cross identity.

theorem ESS.lps_mixed_cross_density_limits_finite {T : ℝ} {a : 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 → ℝ} {s : ℝ} (hULH : CKN.IsLerayHopfSolution T a u Du) (hVLH : CKN.IsLerayHopfSolution T a v Dv) (hU : IsSerrinWeakSolution T a u Du pu) (hV : IsSerrinWeakSolution T a v Dv pv) (hs : 3 < s) (hmix : ∫⁻ (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 ∈ Set.Ioo 0 T, (∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (serrinCrossDensity v Dv pv u Du n (serrinCutoff n)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCrossDensity v Dv pv u Du n (serrinCutoff n) q) Filter.atTop (nhds ((-∫ (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))) ∧ ∀ t ∈ Set.Ioo 0 T, (∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (serrinCrossDensity u Du pu v Dv n (serrinCutoff n)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCrossDensity u Du pu v Dv n (serrinCutoff n) q) Filter.atTop (nhds ((-∫ (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))

Both oriented cross densities have the required finite-exponent integrability and cutoff-mollification limits. The first product is the distinguished velocity against the rival's advective convection.