The Ladyzhenskaya–Prodi–Serrin theorem

The theorem thm:lps: a Leray–Hopf solution satisfying the Serrin condition is unique among Leray–Hopf solutions with its datum and has a representative that is smooth up to the final time. It is assembled from the continuation lemma lem:lps-continuation, the comparison lemma lem:lps-comparison and the smoothing proposition prop:lps-smoothing.

theorem ESS.Main.ladyzhenskayaProdiSerrin (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) : CKN.IsLerayHopfSolution T a u Du → (∃ (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 : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3), CKN.IsLerayHopfSolution T a v Dv → v =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))] u) ∧ ∃ (uSmooth : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), uSmooth =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))] u ∧ ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => uSmooth z) (Set.univ ×ˢ Set.Ioc 0 T)

The Ladyzhenskaya–Prodi–Serrin theorem thm:lps.