Relative energy for a finite Serrin distinguished solution #
The distinguished solution's a.e. energy equality enters as an explicit
hypothesis, matching the provider in EnergyEquality. The competitor uses
only the Leray--Hopf energy inequality.
theorem
ESS.lps_relative_gradient_sq_integrable
{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)
:
The relative gradient square is integrable on the full time slab for two Leray--Hopf velocity fields.
theorem
ESS.lps_finite_relative_energy_zero
{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) < ⊤)
(hEnergyEquality :
∀ᵐ (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 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du z k j * Du z k j)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), lpsComparisonDistanceSq u v t = 0
The finite Serrin cross identity, the distinguished energy equality, the
competitor energy inequality, and the exponent-general slice bound imply that
the two solutions have zero relative energy almost everywhere. The a.e.
energy-equality premise is deliberately explicit; lem:lps-energy-equality supplies it.