The second level of the vorticity bootstrap #
The first derivative of the vorticity flux is square integrable once the velocity gradient is in
L⁴; differentiating the weak vorticity equation and applying the weak local heat gain gives
square-integrable second derivatives of the vorticity (the second level of
thm:vorticity-regularity).
def
ESS.vorticityFluxDeriv
(U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(i j m : Fin 3)
(z : CKN.Foundation.Parabolic.Vec3 × ℝ)
:
The first derivative of the vorticity flux, ∂ₘ(-(uⱼ ωᵢ - ωⱼ uᵢ)).
Equations
- ESS.vorticityFluxDeriv U G Ω1 i j m z = -(G j m z * ESS.vorticityCurl G i z + U j z * Ω1 i m z - (Ω1 j m z * U i z + ESS.vorticityCurl G j z * G i m z))
Instances For
theorem
ESS.vorticityFlux_weakDeriv
{W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)}
(hWo : IsOpen W)
(hWb : Bornology.IsBounded W)
{U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hU : ∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 (MeasureTheory.volume.restrict W))
(hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 (MeasureTheory.volume.restrict W))
(hΩ1 : ∀ (i j : Fin 3), MeasureTheory.MemLp (Ω1 i j) 2 (MeasureTheory.volume.restrict W))
(hdU :
∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ W →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, U i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, G i j y * ψ y)
(hdw :
∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ W →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω1 i j y * ψ y)
(i j m : Fin 3)
(ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
:
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ W →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, -(U j y * vorticityCurl G i y - vorticityCurl G j y * U i y) * CKN.spatialPartial ψ m y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityFluxDeriv U G Ω1 i j m y * ψ y
The weak derivative of the vorticity flux.
theorem
ESS.vorticityFluxDeriv_sq_le
{U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{M : ℝ}
{z : CKN.Foundation.Parabolic.Vec3 × ℝ}
(hz : ∀ (i : Fin 3), |U i z| ≤ M)
(i j m : Fin 3)
:
The pointwise bound of the flux derivative by the fourth power of the gradient and the square of the vorticity derivative.
theorem
ESS.vorticityLevelTwo_heat
{W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)}
(hWo : IsOpen W)
(hWb : Bornology.IsBounded W)
{U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{M : ℝ}
(hU : ∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 (MeasureTheory.volume.restrict W))
(hUb : ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict W, ∀ (i : Fin 3), |U i z| ≤ M)
(hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 (MeasureTheory.volume.restrict W))
(hΩ1 : ∀ (i j : Fin 3), MeasureTheory.MemLp (Ω1 i j) 2 (MeasureTheory.volume.restrict W))
(hF' : ∀ (i j m : Fin 3), MeasureTheory.IntegrableOn (vorticityFluxDeriv U G Ω1 i j m) W MeasureTheory.volume)
(hdU :
∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ W →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, U i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, G i j y * ψ y)
(hdw :
∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ W →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω1 i j y * ψ y)
(hheat :
∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ W →
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityCurl G i z * (-CKN.timePartial ψ z - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j z) = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ j : Fin 3, -(U j z * vorticityCurl G i z - vorticityCurl G j z * U i z) * CKN.spatialPartial ψ j z)
(i m : Fin 3)
(ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
:
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ W →
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω1 i m z * (-CKN.timePartial ψ z - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j z) = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, ∑ j : Fin 3, vorticityFluxDeriv U G Ω1 i j m z * CKN.spatialPartial ψ j z
The weak heat equation for the first derivatives of the vorticity, with the differentiated flux as source.
theorem
ESS.vorticityFluxDeriv_memLp
{μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)}
{U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{M : ℝ}
(hU : ∀ (i : Fin 3), MeasureTheory.MemLp (U i) 2 μ)
(hUb : ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂μ, ∀ (i : Fin 3), |U i z| ≤ M)
(hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) 2 μ)
(hS :
MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => (∑ a : Fin 3, ∑ b : Fin 3, G a b z ^ 2) ^ 2)
μ)
(hΩ1 : ∀ (i j : Fin 3), MeasureTheory.MemLp (Ω1 i j) 2 μ)
(i j m : Fin 3)
:
MeasureTheory.MemLp (vorticityFluxDeriv U G Ω1 i j m) 2 μ
Square integrability of the flux derivative.
theorem
ESS.vorticityLevelTwo
(M K₁ K₄ : ℝ)
:
∃ (K : ℝ),
0 ≤ K ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a t₀ : ℝ) (U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
a + 1 / 16 < t₀ →
t₀ ≤ a + 1 →
(∀ (i : Fin 3),
MeasureTheory.MemLp (U i) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀))) →
(∀ᵐ (z :
CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀), ∀ (i : Fin 3), |U i z| ≤ M) →
(∀ (i j : Fin 3),
MeasureTheory.MemLp (G i j) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀))) →
MeasureTheory.Integrable
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => (∑ i : Fin 3, ∑ j : Fin 3, G i j z ^ 2) ^ 2)
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀)) →
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀, (∑ i : Fin 3, ∑ j : Fin 3, G i j z ^ 2) ^ 2 ≤ K₄ →
(∀ (i j : Fin 3),
MeasureTheory.MemLp (Ω1 i j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀))) →
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀, ∑ i : Fin 3, ∑ j : Fin 3, Ω1 i j z ^ 2 ≤ K₁ →
(∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀, U i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀, G i j y * ψ y) →
(∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀, Ω1 i j y * ψ y) →
(∀ (i : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a t₀ →
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (13 / 16) ×ˢ Set.Ioo a 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₀ (13 / 16) ×ˢ Set.Ioo a t₀, ∑ j : Fin 3,
-(U j z * vorticityCurl G i z - vorticityCurl G j z * U i z) * CKN.spatialPartial ψ j z) →
∃ (Ω2 : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
(∀ (i j k : Fin 3),
MeasureTheory.MemLp (Ω2 i j k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (12 / 16) ×ˢ Set.Ioo (a + 1 / 16) t₀))) ∧ (∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (12 / 16) ×ˢ Set.Ioo (a + 1 / 16) t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (12 / 16) ×ˢ Set.Ioo (a + 1 / 16) t₀, Ω1 i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (12 / 16) ×ˢ Set.Ioo (a + 1 / 16) t₀, Ω2 i j k y * ψ y) ∧ ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (12 / 16) ×ˢ Set.Ioo (a + 1 / 16) t₀, ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, Ω2 i j k y ^ 2 ≤ K
The second level of the bootstrap: square-integrable second derivatives of the vorticity
(the second vorticity level of thm:vorticity-regularity).