The exterior vorticity at the terminal face

lem:vorticity-top-extension: the vorticity of a suitable weak solution which is bounded, with bounded gradient energy, on every unit past cylinder centred in the exterior region {|x| > R₂} × (-2, 0), and whose velocity has zero weak trace at time zero, has a representative continuous on {|x| > R₂} × (-2, 0], vanishing at time zero, bounded, with space-time weak derivatives in L² on bounded sets, satisfying |∂ₜω - Δω| ≤ C (|ω| + |∇ω|).

The representative is glued from the continuous representatives of thm:vorticity-regularity on the half-cylinders below the points of the exterior region, including those with top at time zero; the weak derivatives are glued from a countable family of half-cylinders and a smooth partition of unity.

theorem ESS.vorticityTopExtension (T₂ R₂ M E : ℝ) : 2 < T₂ → 0 < R₂ → 0 ≤ M → 0 ≤ E → ∀ (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 → ℝ), CKN.IsSuitableWeakSolution Set.univ (Set.Ioo (-4 * T₂) 0) 3 U DU q 0 → essSup (fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (U (x, t))) 3 MeasureTheory.volume) (MeasureTheory.volume.restrict (Set.Ioo (-4 * T₂) 0)) < ⊤ → HasZeroDistributionalVelocityTrace U → (∀ (x₁ : CKN.Foundation.Parabolic.Vec3) (t₁ : ℝ), R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x₁ → t₁ ∈ Set.Ioo (-2) 0 → ∃ (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ), IsOpen Ω ∧ IsOpen I ∧ closure (CKN.Foundation.Parabolic.parabolicCylinder x₁ t₁ 1) ⊆ CKN.spaceTimeSet Ω I ∧ CKN.IsSuitableWeakSolution Ω I 3 U DU q 0 ∧ (∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x₁ t₁ 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (U z) ≤ M) ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder x₁ t₁ 1, ‖DU z‖ₑ ^ 2 ≤ ENNReal.ofReal (E ^ 2)) → ∃ (C : ℝ), 0 ≤ C ∧ ∃ (ω : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dω : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2ω : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtω : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), ω =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x} (Set.Ioo (-2) 0))] weakVorticity DU ∧ ContinuousOn ω (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x} (Set.Ioc (-2) 0)) ∧ (∀ (x : CKN.Foundation.Parabolic.Vec3), R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x → ω (x, 0) = 0) ∧ (∀ (x : CKN.Foundation.Parabolic.Vec3), R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x → ∀ t ∈ Set.Ioc (-2) 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (ω (x, t)) ≤ C) ∧ CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x} (Set.Ioo (-2) 0) ω Dω D2ω Dtω ∧ (∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x} (Set.Ioo (-2) 0), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖ω z‖ₑ ^ 2 + ‖Dω z‖ₑ ^ 2 + ‖D2ω z‖ₑ ^ 2 + ‖Dtω z‖ₑ ^ 2 < ⊤) ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x} (Set.Ioo (-2) 0)), (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtω z i - ∑ j : Fin 3, D2ω z i j j) ≤ C * (CKN.Foundation.Parabolic.vec3EuclideanNorm (ω z) + √(CKN.spatialGradientSq ω Dω z))

lem:vorticity-top-extension.