The tested energy inequality with the stretching splitting supplied #
energy_inequality_of_mixed_term_bound assembles eq:aniso:closure:energy from the
enstrophy balance and the two stretching estimates, carrying the splitting of the tested
stretching term as a hypothesis. That splitting is now proved
(cutoffStretching_eq_stretchGTerm_add_mixed_sub_angular), so it is supplied here and the
mixed term is the concrete integral I(t) = ∫ χ² (∂_r u_z) ω_r ω_z of
eq:aniso:closure:mixed. What remains carried is the bound on that integral,
eq:aniso:closure:mixed:bound.
theorem
CIV.energy_inequality_of_mixed_term_bound_of_split
{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ω)
{Cm : ℝ}
(hCm : 0 ≤ Cm)
{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,
∫ (x : CKN.Foundation.Parabolic.Vec3), χ x ^ 2 * stretchMixedTerm u x t ≤ 1 / 4 * cutoffEnstrophyDissipation χ u t + Cm * (W t ^ 2 + 1) * (cutoffEnstrophy χ u t + 1))
:
eq:aniso:closure:energy with the stretching splitting discharged: the only
remaining hypothesis of the assembly is the bound on the mixed term
I(t) = ∫ χ² (∂_r u_z) ω_r ω_z of eq:aniso:closure:mixed.