Smoothness from endpoint velocity control

theorem ESS.essSmooth (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)) < ⊤ → MeasureTheory.MemLp u (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ (∀ (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 full regularity, integrability, and uniqueness conclusion corresponding to manuscript label cor:ess-smooth; this is the consequence of Escauriaza–Seregin– Šverák, Theorem 1.3, together with its smoothness-on-the-closed-top-time form from Theorem 1.2. The smooth representative is viewed on 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 uniqueDiffOn_univ.prod (uniqueDiffOn_Ioc 0 T); thus at t = T within-set derivatives are uniquely determined from times below T.