Vanishing of the vorticity of the blow-up limit

For a suitable solution on ℝ³ × (-12, 0) whose weak vorticity vanishes on the half-space {x₃ > R₂} throughout (-2, 0), CKN's partial regularity and the time projection (lem:time-projection) give, for almost every time, closed balls of regular points on short time intervals; the continuation argument of thm:ess-local (time-slice and spatial unique continuation) then makes the weak vorticity vanish on almost every time slice.

theorem ESS.essLocal_interiorVorticityZero {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 → ℝ} (hsws : CKN.IsSuitableWeakSolution Set.univ (Set.Ioo (-12) 0) 3 U DU q 0) (R₂ : ℝ) (hR₂ : 0 < R₂) (hseed : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | R₂ < x 2} (Set.Ioo (-2) 0)), weakVorticity DU z = 0) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-2) 0), (fun (x : CKN.Foundation.Parabolic.Vec3) => weakVorticity DU (x, t)) =ᵐ[MeasureTheory.volume] 0

The weak vorticity of a suitable solution on ℝ³ × (-12, 0) vanishing on the half-space {x₃ > R₂} over (-2, 0) vanishes on almost every time slice of (-2, 0).