The starting data of the vorticity bootstrap

For a suitable weak solution on a neighbourhood of the closed unit past cylinder, the velocity, its gradient, the weak vorticity and the vorticity flux are square integrable on the open unit box below the top, the gradient is the weak spatial gradient of the velocity there, the velocity is weakly divergence free, and each vorticity component solves the weak heat equation with a divergence-form source (lem:vorticity-weak-eq, used in thm:vorticity-regularity).

theorem ESS.vorticityUnitBox_subset_cylinder (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) : CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ ⊆ CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1

The open unit box below the top of the unit past cylinder lies in that cylinder.

theorem ESS.vorticity_exists_localBox_of_closure {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hIord : I.OrdConnected) {x₀ : CKN.Foundation.Parabolic.Vec3} {t₀ : ℝ} (hcl : closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1) ⊆ CKN.spaceTimeSet Ω I) : ∃ (Ω' : Set CKN.Foundation.Parabolic.Vec3) (J : Set ℝ), CKN.localBox Ω I Ω' J ∧ CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ ⊆ CKN.spaceTimeSet Ω' J

A local box of a suitable solution containing the closed unit cylinder.

theorem ESS.vorticityBase_memLp {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (h : CKN.IsSuitableWeakSolution Ω I q u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) (hΩ : IsOpen Ω) (hI : IsOpen I) {x₀ : CKN.Foundation.Parabolic.Vec3} {t₀ : ℝ} (hcl : closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1) ⊆ CKN.spaceTimeSet Ω I) : (∀ (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₀))

Square integrability of the velocity and gradient components on the open unit box.

theorem ESS.vorticityBase_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {x₀ : CKN.Foundation.Parabolic.Vec3} {t₀ M : ℝ} (hM : ∀ᵐ (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) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀), ∀ (i : Fin 3), |u z i| ≤ M

The bound of the velocity components on the open unit box.

theorem ESS.vorticityBase_energy {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {x₀ : CKN.Foundation.Parabolic.Vec3} {t₀ E : ℝ} (hDu : ∀ (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₀))) (hE : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1, ‖Du z‖ₑ ^ 2 ≤ ENNReal.ofReal (E ^ 2)) : ∫ (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 ≤ 9 * E ^ 2

The gradient energy on the open unit box is controlled by the energy on the cylinder.

theorem ESS.vorticity_setIntegral_congr_of_vanish {S T : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hST : S ⊆ T) (hzero : ∀ z ∉ S, h z = 0) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in S, h z = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in T, h z

Set integrals of functions vanishing off a subset agree.

theorem ESS.vorticityBase_weakGradient {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (h : CKN.IsSuitableWeakSolution Ω I q u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) (hΩ : IsOpen Ω) (hI : IsOpen I) {x₀ : CKN.Foundation.Parabolic.Vec3} {t₀ : ℝ} (hcl : closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1) ⊆ CKN.spaceTimeSet Ω I) (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

The gradient is the weak spatial gradient of the velocity on the open unit box.

theorem ESS.vorticityBase_div {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (h : CKN.IsSuitableWeakSolution Ω I q u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) {x₀ : CKN.Foundation.Parabolic.Vec3} {t₀ : ℝ} (hcl : closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1) ⊆ CKN.spaceTimeSet Ω I) (ψ : 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

The velocity is weakly divergence free on the open unit box.

theorem ESS.vorticity_partials_zero (z : CKN.Foundation.Parabolic.Vec3 × ℝ) (j : Fin 3) : CKN.timePartial (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0) z = 0 ∧ CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0) j z = 0 ∧ CKN.spatialSecondPartial (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0) j j z = 0

Coordinate derivatives of the zero function vanish.

theorem ESS.vorticityBase_heat {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (h : CKN.IsSuitableWeakSolution Ω I q u Du p fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => 0) (hΩ : IsOpen Ω) (hI : IsOpen I) {x₀ : CKN.Foundation.Parabolic.Vec3} {t₀ : ℝ} (hcl : closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ 1) ⊆ CKN.spaceTimeSet Ω I) (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

Each vorticity component solves the weak heat equation with the divergence-form source given by the vorticity flux on the open unit box (lem:vorticity-weak-eq).