The starting data of the vorticity estimates below an exterior point

For a solution which is suitable, bounded and of bounded gradient energy near every unit past cylinder with exterior centre and top time in (-2, 0), the velocity, its gradient, the weak gradient identity, the divergence identity and the weak vorticity equation hold on every open unit box below an exterior top point with top time in (-2, 0]; at the top time 0 the box is exhausted by the boxes below the times -1/(n+2) (lem:vorticity-top-extension).

theorem ESS.vorticityTopData_energy {W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {K : ℝ} (hK : 0 ≤ K) (hDu : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du z i j) 2 (MeasureTheory.volume.restrict W)) (hE : ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ‖Du z‖ₑ ^ 2 ≤ ENNReal.ofReal K) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ i : Fin 3, ∑ j : Fin 3, Du z i j ^ 2 ≤ 9 * K

The gradient energy on a set is controlled by the Lebesgue integral of the squared norm.

theorem ESS.vorticityTopData_times : (∀ (n : ℕ), -(1 / 2) ≤ -(1 / (↑n + 2)) ∧ -(1 / (↑n + 2)) < 0) ∧ (Monotone fun (n : ℕ) => -(1 / (↑n + 2))) ∧ ∀ t < 0, ∃ (n : ℕ), t < -(1 / (↑n + 2))

The times -1/(n+2) increase to 0 inside [-1/2, 0).

theorem ESS.vorticityExterior_boxData {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₁) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioc (-2) 0) : (∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => U z i) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀))) ∧ (∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => DU z i j) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀))) ∧ (∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀), ∀ (i : Fin 3), |U z i| ≤ M) ∧ ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, ∑ i : Fin 3, ∑ j : Fin 3, DU z i j ^ 2 ≤ 18 * E ^ 2 ∧ (∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, U z i * CKN.spatialPartial ψ j z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, DU z i j * ψ z) ∧ (∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, ∑ i : Fin 3, U z i * CKN.spatialPartial ψ i z = 0) ∧ ∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ → ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, weakVorticity DU z i * (-CKN.timePartial ψ z - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j z) = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₁ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, ∑ j : Fin 3, -vorticityFlux U DU z j i * CKN.spatialPartial ψ j z

The data of the vorticity estimates on the unit box below an exterior top point.