Relative cross identity for a finite Serrin solution #
The finite mixed norms make both oriented weak cross-testings integrable. The slice cancellation then combines them into the relative convection form.
theorem
ESS.lps_finite_relative_cross_identity
{T s : ℝ}
{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 → ℝ}
(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 : ℝ) ∂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, a x k * a x k = (-∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), lpsRelativeConvection u v Du Dv z) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du z k j * Dv z k j) ∧ MeasureTheory.Integrable (lpsRelativeConvection u v Du Dv)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))
The finite Serrin cross-testings combine into the relative cross identity.
The two oriented densities are u · ((v · ∇)v) and v · ((u · ∇)u);
their cancellation uses only the integrable products in the slice lemma.