The product bound at the third level #
The product of the squared velocity gradient with the squared second derivatives of the velocity
and first derivatives of the vorticity is integrable, with a bound by the data (the H³ product
estimate of lem:vorticity-products, in the form used by thm:vorticity-regularity): at every
time the gradient of a smooth approximation is bounded by the H² embedding and the chain of
div–curl estimates, and Fatou's lemma passes the bound to the limit.
Euclidean balls of equal radii have equal volume.
theorem
ESS.vorticity_setIntegral_sq_le_of_bound
{x₀ : CKN.Foundation.Parabolic.Vec3}
{r M : ℝ}
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : Continuous f)
(hM : ∀ (x : CKN.Foundation.Parabolic.Vec3), |f x| ≤ M)
:
∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ r, f x ^ 2 ≤ M ^ 2 * (MeasureTheory.volume (CKN.Foundation.Parabolic.vec3Ball 0 r)).toReal
A bounded function has square integral on a ball at most the squared bound times the volume.
theorem
ESS.vorticityLevelThree_SP
(M Kw K1 K0 K2 K3 : ℝ)
(hM : 0 ≤ M)
:
∃ (K : ℝ),
0 ≤ K ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a t₀ : ℝ) (U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(G Ω1 F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(D2 Ω2 F' : Fin 3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
a + 1 / 32 < t₀ →
t₀ ≤ a + 1 →
(∀ (i : Fin 3),
MeasureTheory.MemLp (U i) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ᵐ (z :
CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ 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₀ (48 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j k : Fin 3),
MeasureTheory.MemLp (D2 i j k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j : Fin 3),
MeasureTheory.MemLp (Ω1 i j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j k : Fin 3),
MeasureTheory.MemLp (Ω2 i j k) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j : Fin 3),
MeasureTheory.MemLp (F i j) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j m : Fin 3),
MeasureTheory.MemLp (F' i j m) 2
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀))) →
(∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, U i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, G i j y * ψ y) →
(∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, G i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, D2 i j k y * ψ y) →
(∀ (i j : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, vorticityCurl G i y * CKN.spatialPartial ψ j y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, Ω1 i j y * ψ y) →
(∀ (i j k : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, Ω1 i j y * CKN.spatialPartial ψ k y = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, Ω2 i j k y * ψ y) →
(∀ (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a 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₀ (48 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, vorticityCurl G i y * (-CKN.timePartial ψ y - ∑ j : Fin 3, CKN.spatialSecondPartial ψ j j y) = -∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, ∑ j : Fin 3, F i j y * CKN.spatialPartial ψ j y) →
(∀ (i m : Fin 3) (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆
CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀ →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a 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₀ (48 / 64) ×ˢ Set.Ioo a t₀, ∑ j : Fin 3, F' i j m y * CKN.spatialPartial ψ j y) →
(∀ (i : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, vorticityCurl G i y ^ 2 + ∑ j : Fin 3, F i j y ^ 2 ≤ Kw) →
(∀ (i m : Fin 3),
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, Ω1 i m y ^ 2 + ∑ j : Fin 3, F' i j m y ^ 2 ≤ K1) →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, ∑ i : Fin 3, ∑ j : Fin 3, G i j y ^ 2 ≤ K0 →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, D2 i j k y ^ 2 ≤ K2 →
∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (48 / 64) ×ˢ Set.Ioo a t₀, ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, Ω2 i j k y ^ 2 ≤ K3 →
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))
(MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (a + 1 / 32) t₀)) ∧ ∫ (y : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ (43 / 64) ×ˢ Set.Ioo (a + 1 / 32) t₀, (∑ 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) ≤ K
The third-level product bound.