The Serrin regularity criterion

theorem ESS.serrinCriterion (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 → essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3) (MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤ ∨ (∃ (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 regularity criterion cor:serrin-criterion over the whole range 3 ≤ s ≤ ∞: a Leray–Hopf solution on [0,T] in L^ℓ(0,T;L^s(ℝ³)) with 3/s + 2/ℓ = 1 is the only Leray–Hopf solution with its datum and agrees almost everywhere with a function that is infinitely differentiable (C^∞; the exponent (⊤ : ℕ∞), not ω) on ℝ³ × (0,T], with one-sided derivatives at T. The hypothesis is a disjunction of the endpoint s = 3 (L^∞_t L³_x, the Escauriaza–Seregin–Šverák case, cor:ess-smooth), the finite range 3 < s < ∞ with ℓ = 2s/(s−3) and the endpoint s = ∞ (L²_t L^∞_x) — the last two being the Ladyzhenskaya–Prodi–Serrin cases of thm:lps.