Uniqueness in the finite Serrin branch #
The distinguished Leray–Hopf solution supplies the a.e. energy equality; the finite mixed-norm cross identity and relative-energy estimate then force the competitor to agree with it almost everywhere.
theorem
ESS.lps_zero_relative_distance_implies_ae_eq
{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}
(hU : CKN.IsLerayHopfSolution T a u Du)
(hV : CKN.IsLerayHopfSolution T a v Dv)
(hZero : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), lpsComparisonDistanceSq u v t = 0)
:
v =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))] u
Zero relative slice energy almost everywhere implies equality of the space-time velocity fields almost everywhere.
theorem
ESS.lps_finite_leray_hopf_uniqueness
{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}
(hU : CKN.IsLerayHopfSolution T a u Du)
(hV : CKN.IsLerayHopfSolution T a v Dv)
(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) < ⊤)
:
v =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))] u
Weak–strong uniqueness for the finite branch of the Serrin condition. The competitor is assumed only to be Leray–Hopf; D2 supplies the distinguished solution's a.e. energy equality.