The conclusions of the vorticity regularity theorem on a product box #
From the velocity, its weak gradient, the velocity bound, the gradient energy and the weak
vorticity equation on a unit box, the vorticity has on the box B_{1/2} × (t₀ - 1/4, t₀) a
representative which is continuous and bounded up to the top time, space-time weak derivatives
in L², and satisfies the differential inequality of thm:vorticity-regularity.
theorem
ESS.vorticityRegularity_box
(M K₀ : ℝ)
(hM : 0 ≤ M)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
(∀ (i : Fin 3),
MeasureTheory.MemLp (U i) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀))) →
(∀ (i j : Fin 3),
MeasureTheory.MemLp (G i j) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀))) →
(∀ᵐ (z :
CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀), ∀ (i : Fin 3), |U i z| ≤ M) →
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, ∑ i : Fin 3, ∑ j : Fin 3, G i j z ^ 2 ≤ K₀ →
(∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, U i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, G i j y * ψ y) →
(∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ 1 ×ˢ Set.Ioo (t₀ - 1) t₀, ∑ i : Fin 3, U i y * CKN.spatialPartial ψ i y = 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₀, vorticityCurl G i z * (-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,
-(U j z * vorticityCurl G i z - vorticityCurl G j z * U i z) * CKN.spatialPartial ψ j z) →
∃ (ω : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (Ω1 :
Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (Ω2 :
Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (Dt :
Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
(∀ (i : Fin 3),
ContinuousOn (ω i)
({x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ 1 / 2} ×ˢ Set.Icc (t₀ - 1 / 4) t₀)) ∧ (∀ (i : Fin 3),
∀
z ∈
{x : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ 1 / 2} ×ˢ Set.Icc (t₀ - 1 / 4) t₀,
|ω i z| ≤ C) ∧ (∀ (i : Fin 3),
ω
i =ᵐ[MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀)]
vorticityCurl G i) ∧ (∀ (i : Fin 3),
MeasureTheory.MemLp (ω i) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀))) ∧ (∀ (i j : Fin 3),
MeasureTheory.MemLp (Ω1 i j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀))) ∧ (∀ (i j k : Fin 3),
MeasureTheory.MemLp (Ω2 i j k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀))) ∧ (∀ (i : Fin 3),
MeasureTheory.MemLp (Dt i) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀))) ∧ (∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀, ω i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀, Ω1 i j y * ψ y) ∧ (∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀, Ω1 i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀, Ω2 i j k y * ψ y) ∧ (∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀, ω i y * CKN.timePartial ψ y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀, Dt i y * ψ y) ∧ ∀ᵐ (z :
CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (1 / 2) ×ˢ Set.Ioo (t₀ - 1 / 4) t₀), ∀ (i : Fin 3),
|Dt i z - ∑ j : Fin 3, Ω2 i j j z| ≤ C * (∑ l : Fin 3, |ω l z| + ∑ a : Fin 3, ∑ b : Fin 3, |Ω1 a b z|)
thm:vorticity-regularity on the product box, for fields on Vec3 × ℝ.