The terminal value of the vorticity

If the velocity has zero weak trace at time zero, the continuous representative of the vorticity below an exterior top point vanishes at the top time (lem:vorticity-top-extension, trace identification): the pairing of the representative with a spatial test is continuous up to the top time, agrees on almost every slice with the pairing of the velocity with the curl of the test, and the latter tends to zero.

theorem ESS.vorticityTopZero_ae_slice {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 → ℝ} {R₂ M E : ℝ} (hfam : ∀ (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)) {x₁ : CKN.Foundation.Parabolic.Vec3} (hx₁ : R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x₁) {φ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφB : tsupport φ ⊆ CKN.Foundation.Parabolic.vec3Ball x₁ 1) : ∀ᵐ (t : ℝ), t ∈ Set.Iio 0 → t ∈ Set.Ioi (-1) → ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, weakVorticity DU (x, t) i * φ x i = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i * spatialTestCurl φ x i

The weak curl identity on almost every slice below an exterior top point.

theorem ESS.vorticityTop_zero {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 → ℝ} {R₂ M E : ℝ} (hfam : ∀ (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)) (htrace : HasZeroDistributionalVelocityTrace U) {x₁ : CKN.Foundation.Parabolic.Vec3} (hx₁ : R₂ < CKN.Foundation.Parabolic.vec3EuclideanNorm x₁) {ω : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {C : ℝ} (hωc : ∀ (i : Fin 3), ContinuousOn (ω i) ({x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₁) ≤ 1 / 2} ×ˢ Set.Icc (0 - 1 / 4) 0)) (hωb : ∀ (i : Fin 3), ∀ z ∈ {x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₁) ≤ 1 / 2} ×ˢ Set.Icc (0 - 1 / 4) 0, |ω i z| ≤ C) (hωae : ∀ (i : Fin 3), ω i =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₁ (1 / 2) ×ˢ Set.Ioo (0 - 1 / 4) 0)] vorticityCurl (fun (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => DU z i j) i) (y : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x₁) < 1 / 2 → ∀ (i : Fin 3), ω i (y, 0) = 0

The continuous representative of the vorticity below an exterior top point vanishes at the top time.