Ladyzhenskaya–Prodi–Serrin regularity #
The Ladyzhenskaya–Prodi–Serrin regularity and uniqueness theorem, corresponding
to manuscript label thm:lps; see Robinson–Rodrigo–Sadowski, Theorems 8.17
and 8.19, and Escauriaza–Seregin–Šverák, Theorem 1.2. For finite s > 3, the
hypothesis is the mixed norm L^ℓ_t L^s_x with ℓ = 2s/(s-3); the second
alternative is L²_t L^∞_x. The smooth representative uses the Euclidean
product Vec3 × ℝ, definitionally the CKN carrier ParabolicPoint, so
ContDiffOn uses the ordinary space-time differentiable structure. It is
infinitely differentiable (C^∞; the exponent (⊤ : ℕ∞), not ω). The set
univ × Ioc 0 T has UniqueDiffOn by the product of uniqueDiffOn_univ and
uniqueDiffOn_Ioc; thus at t = T within-set derivatives are uniquely
determined from times below T.