Two-branch Leray–Hopf uniqueness

Weak–strong uniqueness among Leray–Hopf solutions under either Serrin condition of the Ladyzhenskaya–Prodi–Serrin theorem (thm:lps).

theorem ESS.lps_leray_hopf_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) (hSerrin : (∃ (s : ℝ), 3 < s ∧ ∫⁻ (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 : ℝ) in Set.Ioo 0 T, essSup (fun (x : CKN.Foundation.Parabolic.Vec3) => ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)))) MeasureTheory.volume ^ 2 < ⊤) : v =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))] u

Weak–strong uniqueness under either Serrin condition of thm:lps: a Leray–Hopf solution v with the same datum as a Leray–Hopf solution u that is in L^ℓ_t L^s_x with 3/s + 2/ℓ = 1, 3 < s < ∞, or in L²_t L∞_x, agrees with u almost everywhere.