Smoothing of strong solutions

prop:lps-smoothing: a strong solution on [t₀, t₁] has a representative that is C^∞ on ℝ³ × (t₀, t₁].

theorem ESS.lps_smoothing {t₀ t₁ : ℝ} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (h : IsLpsStrongSolution t₀ t₁ U DU p) : ∃ (R : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), R =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] U ∧ ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => R z) (Set.univ ×ˢ Set.Ioc t₀ t₁)

prop:lps-smoothing: a strong solution of the Navier–Stokes equations on ℝ³ × (t₀, t₁) agrees almost everywhere with a representative that is C^∞ on ℝ³ × (t₀, t₁].