Weak–strong uniqueness for Leray–Hopf solutions #
Two Leray–Hopf solutions with the same datum agree almost everywhere on the
slab when one of them lies in space-time L⁵: lem:pv-serrin-uniqueness. The
comparison uses only the energy inequality of the other solution.
theorem
ESS.serrin_lintegral_eucl_sq
{w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hw : MeasureTheory.MemLp w 2 MeasureTheory.volume)
:
∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (w x)) ^ 2 = ENNReal.ofReal (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, w x k * w x k)
theorem
ESS.lerayHopf_energy_inequality_real
{T : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hLH : CKN.IsLerayHopfSolution T a u Du)
{t : ℝ}
(ht : t ∈ Set.Icc 0 T)
(hut : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume)
:
The energy inequality of a Leray–Hopf solution in real form, at every time whose slice is square integrable.
theorem
ESS.lerayHopf_serrin_uniqueness
{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)
(hu5 :
MeasureTheory.MemLp u (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
u =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))] v
Weak–strong uniqueness for Leray–Hopf solutions with the same datum, one of
which lies in space-time L⁵ (lem:pv-serrin-uniqueness).