Energy Inequality Of Mixed Term #
Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.
theorem
CIV.energy_inequality_of_mixed_term_bound
{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)
(hMf : ForceC2Bounded f)
(haxi : IsAxisymmetricOn u 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)
{Mu Mω : ℝ}
(hMu : 0 ≤ Mu)
(hubd : ∀ x ∈ A, ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3), |u (x, t) i| ≤ Mu)
(hωbd : ∀ x ∈ A, ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3), |vorticityField u (x, t) i| ≤ Mω)
{Mix : ℝ → ℝ}
{Cm : ℝ}
(hCm : 0 ≤ Cm)
(hsplit :
∀ t ∈ Set.Ioo t₀ 0,
cutoffStretching χ u t = (∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * stretchGTerm u x t) + Mix t - ∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * (2 * stretchAngularSwirl u x t * curlComp u 1 (meridional (polarR x) (x 2), t)))
{G W : ℝ → ℝ}
(hGnn : ∀ (t : ℝ), 0 ≤ G t)
(hG :
∀ t ∈ Set.Ioo t₀ 0,
∀ (x₁ x₃ : ℝ),
meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → meridionalQuantity u (meridional x₁ x₃, t) ≤ G t)
(hW :
∀ t ∈ Set.Ioo t₀ 0,
∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → |u (meridional x₁ x₃, t) 1| ≤ W t)
(hmix :
∀ t ∈ Set.Ioo t₀ 0,
Mix t ≤ 1 / 4 * cutoffEnstrophyDissipation χ u t + Cm * (W t ^ 2 + 1) * (cutoffEnstrophy χ u t + 1))
:
eq:aniso:closure:energy, the tested enstrophy inequality of lem:aniso:closure,
conditioned on the mixed-term bound of eq:aniso:closure:mixed:bound and on the splitting of the
tested stretching term, both taken as explicit hypotheses. Both are proved separately: the
splitting is supplied in energy_inequality_of_mixed_term_bound_of_split, and the mixed-term
bound is step_closure_mixed_term.
The three pieces — cutoff_enstrophy_balance, stretchGTerm_integral_le,
stretchAngularTerm_integral_abs_le — are assembled into the exact shape
deriv Y + M ≤ C_*(G + W² + 1)(Y + 1).