The chain of interior estimates for the vorticity #
From the velocity, its weak gradient, the velocity bound, the gradient energy and the weak
vorticity equation on a unit box, the interior estimates of thm:vorticity-regularity produce,
on a smaller box, the first and second spatial derivatives of the vorticity and the second
derivatives of the velocity, the heat equations they solve, and bounds depending only on the
velocity bound and the gradient energy.
theorem
ESS.vorticityStages
(M K₀ : ℝ)
(hM : 0 ≤ M)
:
∃ (Kw : ℝ) (K1 : ℝ) (K2 : ℝ),
∀ (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) →
∃ (Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (D2 :
Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (Ω2 :
Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
(∀ (i j k : Fin 3),
MeasureTheory.MemLp (D2 i j k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀))) ∧ (∀ (i j : Fin 3),
MeasureTheory.MemLp (Ω1 i j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀))) ∧ (∀ (i j k : Fin 3),
MeasureTheory.MemLp (Ω2 i j k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀))) ∧ (∀ (i j m : Fin 3),
MeasureTheory.MemLp (vorticityFluxDeriv U G Ω1 i j m) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀))) ∧ (∀ (i j m k : Fin 3),
MeasureTheory.MemLp (vorticityFluxDeriv2 U G Ω1 D2 Ω2 i j m k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀))) ∧ (∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, G i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, D2 i j k y * ψ y) ∧ (∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, Ω1 i j y * ψ y) ∧ (∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, Ω1 i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, Ω2 i j k y * ψ y) ∧ (∀ (i m : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, Ω1 i m y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, ∑ j : Fin 3,
vorticityFluxDeriv U G Ω1 i j m y * CKN.spatialPartial ψ j y) ∧ (∀ (i m k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, Ω2 i m k y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32)
t₀, ∑ j : Fin 3,
vorticityFluxDeriv2 U G Ω1 D2 Ω2 i j m k y * CKN.spatialPartial ψ j y) ∧ (∀ (i : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, vorticityCurl G i y ^ 2 + ∑ j : Fin 3,
(-(U j y * vorticityCurl G i y - vorticityCurl G j y * U i y)) ^ 2 ≤ Kw) ∧ (∀ (i m : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, Ω1 i m y ^ 2 + ∑ j : Fin 3, vorticityFluxDeriv U G Ω1 i j m y ^ 2 ≤ K1) ∧ ∀ (i m k : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (t₀ - 1 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 16 + 1 / 32) t₀, Ω2 i m k y ^ 2 + ∑ j : Fin 3, vorticityFluxDeriv2 U G Ω1 D2 Ω2 i j m k y ^ 2 ≤ K2
The interior estimates of thm:vorticity-regularity up to the second derivatives of the
vorticity.