Ess Local Proof Global Suitable

Local endpoint regularity through vorticity estimates and backward uniqueness.

theorem ESS.essLocal_globalSuitable_of_local (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hlocal : ∀ (R a : ℝ), 0 < R → a < 0 → CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo a 0) 3 U DU q 0) (a : ℝ) (ha : a < 0) : CKN.IsSuitableWeakSolution Set.univ (Set.Ioo a 0) 3 U DU q 0

Local suitability on every origin-centred past cylinder yields the global CKN suitable-solution predicate on any finite past interval.