eq:aniso:closure:elliptic with velocity-bound hypotheses discharged from an annulus bound #
This file specialises the two elliptic bounds of eq:aniso:closure:elliptic (the gradient
and Hessian estimates of lem:aniso:closure) to the situation where the velocity bounds on the
closed set A come directly from an order‑≤2 multiPartial annulus bound of
lem:aniso:annulus, bypassing the need to supply separate hubd/hubd2 hypotheses.
The three commutator witnesses (integral_cutoff_sq_fderiv_le,
integral_cutoff_sq_fderiv_fderiv_le, integral_sq_fderiv_fderiv_smul_le) are already stated
in their respective source modules and are applied here without redefinition. Only the annulus
subset A and the cutoff data remain abstract, following the same pattern as
CIV.cutoff_enstrophy_balance_of_multiPartial_le in CutoffEnstrophyBalanceAnnulusBound.lean.
theorem
CIV.integral_cutoff_sq_spatialPartial_le_of_multiPartial_le
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsol : IsClassicalSolutionOn u p f unitCylinder)
{χ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hχ : ContDiff ℝ (↑⊤) χ)
(hχs : HasCompactSupport χ)
{ρ : ℝ}
(hρU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ)
(hρ1 : CKN.Foundation.Parabolic.vec3Ball 0 ρ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1)
{t₀ : ℝ}
(ht₀ : t₀ ∈ Set.Ioo (-1) 0)
{A : Set CKN.Foundation.Parabolic.Vec3}
(hAcl : IsClosed A)
(hχA : ∀ x ∉ A, fderiv ℝ χ x = 0)
{Rm Rp Mu : ℝ}
(hAsub :
A ⊆
{x : CKN.Foundation.Parabolic.Vec3 | Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp})
(hbound :
∀ (x : CKN.Foundation.Parabolic.Vec3),
Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x →
CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp →
∀ t ∈ Set.Ioo t₀ 0,
∀ (i : Fin 3) (α : Fin 3 → ℕ),
α 0 + α 1 + α 2 ≤ 2 →
|multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ Mu)
:
theorem
CIV.integral_cutoff_sq_spatialSecondPartial_le_of_multiPartial_le
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsol : IsClassicalSolutionOn u p f unitCylinder)
{χ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hχ : ContDiff ℝ (↑⊤) χ)
(hχs : HasCompactSupport χ)
{ρ : ℝ}
(hρU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ)
(hρ1 : CKN.Foundation.Parabolic.vec3Ball 0 ρ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1)
{t₀ : ℝ}
(ht₀ : t₀ ∈ Set.Ioo (-1) 0)
{A : Set CKN.Foundation.Parabolic.Vec3}
(hAcl : IsClosed A)
(hχA : ∀ x ∉ A, fderiv ℝ χ x = 0)
{Rm Rp Mu : ℝ}
(hAsub :
A ⊆
{x : CKN.Foundation.Parabolic.Vec3 | Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp})
(hbound :
∀ (x : CKN.Foundation.Parabolic.Vec3),
Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x →
CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp →
∀ t ∈ Set.Ioo t₀ 0,
∀ (i : Fin 3) (α : Fin 3 → ℕ),
α 0 + α 1 + α 2 ≤ 2 →
|multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ Mu)
:
theorem
CIV.exists_C_cutoff_sq_spatialPartial_and_spatialSecondPartial_le_of_multiPartial_le
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsol : IsClassicalSolutionOn u p f unitCylinder)
{χ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hχ : ContDiff ℝ (↑⊤) χ)
(hχs : HasCompactSupport χ)
{ρ : ℝ}
(hρU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ)
(hρ1 : CKN.Foundation.Parabolic.vec3Ball 0 ρ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1)
{t₀ : ℝ}
(ht₀ : t₀ ∈ Set.Ioo (-1) 0)
{A : Set CKN.Foundation.Parabolic.Vec3}
(hAcl : IsClosed A)
(hχA : ∀ x ∉ A, fderiv ℝ χ x = 0)
{Rm Rp Mu : ℝ}
(hAsub :
A ⊆
{x : CKN.Foundation.Parabolic.Vec3 | Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp})
(hbound :
∀ (x : CKN.Foundation.Parabolic.Vec3),
Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x →
CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp →
∀ t ∈ Set.Ioo t₀ 0,
∀ (i : Fin 3) (α : Fin 3 → ℕ),
α 0 + α 1 + α 2 ≤ 2 →
|multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ Mu)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ t ∈ Set.Ioo t₀ 0,
∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * ∑ i : Fin 3,
∑ j : Fin 3,
CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j (x, t) ^ 2 ≤ C * (cutoffEnstrophy χ u t + 1) ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * ∑ i : Fin 3,
∑ j : Fin 3,
∑ k : Fin 3,
CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j k (x, t) ^ 2 ≤ C * (cutoffEnstrophyDissipation χ u t + 1)