The third level of the vorticity bootstrap

The second derivative of the vorticity flux is square integrable by the third-level product bound; differentiating the weak heat equation of the first derivatives of the vorticity gives the weak heat equation of the second derivatives (the third level of thm:vorticity-regularity).

def ESS.vorticityFluxDeriv2 (U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (D2 Ω2 : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (i j m k : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The second derivative of the vorticity flux, ∂ₖ ∂ₘ(-(uⱼ ωᵢ - ωⱼ uᵢ)).

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.vorticityFluxDeriv_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 × ℝ → ℝ} {D2 Ω2 : Fin 3 → 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)) (hD2 : ∀ (i j k : Fin 3), MeasureTheory.MemLp (D2 i j k) 2 (MeasureTheory.volume.restrict W)) (hΩ1 : ∀ (i j : Fin 3), MeasureTheory.MemLp (Ω1 i j) 2 (MeasureTheory.volume.restrict W)) (hΩ2 : ∀ (i j k : Fin 3), MeasureTheory.MemLp (Ω2 i j k) 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) (hdG : ∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, G i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, D2 i j k 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) (hdΩ1 : ∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω1 i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, Ω2 i j k y * ψ y) (i j m k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityFluxDeriv U G Ω1 i j m y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in W, vorticityFluxDeriv2 U G Ω1 D2 Ω2 i j m k y * ψ y

The weak derivative of the flux derivative.

theorem ESS.vorticityFluxDeriv2_sq_le {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D2 Ω2 : Fin 3 → 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 k : Fin 3) : vorticityFluxDeriv2 U G Ω1 D2 Ω2 i j m k z ^ 2 ≤ 64 * ((∑ a : Fin 3, ∑ b : Fin 3, G a b z ^ 2) * (∑ a : Fin 3, ∑ b : Fin 3, ∑ c : Fin 3, D2 a b c z ^ 2 + ∑ a : Fin 3, ∑ b : Fin 3, Ω1 a b z ^ 2)) + 16 * M ^ 2 * ∑ a : Fin 3, ∑ b : Fin 3, ∑ c : Fin 3, Ω2 a b c z ^ 2

The pointwise bound of the second flux derivative.

theorem ESS.vorticityFluxDeriv2_memLp {μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)} {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {G Ω1 : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D2 Ω2 : Fin 3 → 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 μ) (hD2 : ∀ (i j k : Fin 3), MeasureTheory.MemLp (D2 i j k) 2 μ) (hΩ1 : ∀ (i j : Fin 3), MeasureTheory.MemLp (Ω1 i j) 2 μ) (hΩ2 : ∀ (i j k : Fin 3), MeasureTheory.MemLp (Ω2 i j k) 2 μ) (hSP : MeasureTheory.Integrable (fun (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => (∑ i : Fin 3, ∑ j : Fin 3, G i j y ^ 2) * (∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, D2 i j k y ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, Ω1 i j y ^ 2)) μ) (i j m k : Fin 3) : MeasureTheory.MemLp (vorticityFluxDeriv2 U G Ω1 D2 Ω2 i j m k) 2 μ

Square integrability and the bound of the second flux derivative from the product bound.