Global endpoint regularity

The global Escauriaza–Seregin–Šverák theorem thm:ess-global: a Leray–Hopf solution on ℝ³ × (0, T) that is bounded in L³ in space uniformly in time has no singular points. The local theorem thm:ess-local is applied to rescalings of the solution around each point, with the associated pressure of thm:assoc-pressure and its L^∞ L^{3/2} bound from lem:assoc-pressure-L3.

theorem ESS.Main.essGlobal (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)) < ⊤ → CKN.SingularSet Set.univ (Set.Ioo 0 T) u = ∅

The global Escauriaza–Seregin–Šverák regularity theorem thm:ess-global.