closure_enstrophy_decay_of_exists_energy_inequality is exists_closure_gronwall_bound_of_exists_energy_inequality for the cutoff enstrophy cutoffEnstrophy χ u and its dissipation cutoffEnstrophyDissipation χ u: it composes the substitution step deriv_le_of_closure_energy of eq:aniso:closure:energy with the Grönwall step closure_gronwall_bound of lem:aniso:closure, so that the energy inequality in the form ∃ Cstar ≥ 1, … together with the G, W decay data gives the enstrophy decay Y + 1 ≤ C' (−t)^{−C_*η}. closure_enstrophy_decay_sixteenth_eta_of_exists_energy_inequality is the specialization to the manuscript's choice η = 1/(16 C_*), for which the decay exponent is the universal constant 1/16 (exists_closure_gronwall_bound_sixteenth_eta), and closure_enstrophy_decay_of_mixed_term_bound obtains the energy inequality from CIV.energy_inequality_of_mixed_term_bound.

theorem CIV.closure_enstrophy_decay_of_exists_energy_inequality {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) (hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {tη η Cη : ℝ} (htη : tη ∈ Set.Ioo (-1) 0) (hη : 0 < η ∧ 2 * η < 1) (hCη : 0 ≤ Cη) {G W : ℝ → ℝ} (hG : ∀ t ∈ Set.Ioo tη 0, G t ≤ η / -t) (hW0 : ∀ t ∈ Set.Ioo tη 0, 0 ≤ W t) (hW : ∀ t ∈ Set.Ioo tη 0, W t ≤ Cη * (-t) ^ (-η)) (hex : ∃ (Cstar : ℝ), 1 ≤ Cstar ∧ ∀ t ∈ Set.Ioo tη 0, deriv (cutoffEnstrophy χ u) t + cutoffEnstrophyDissipation χ u t ≤ Cstar * (G t + W t ^ 2 + 1) * (cutoffEnstrophy χ u t + 1)) : ∃ (Cstar : ℝ), 1 ≤ Cstar ∧ ∃ (C' : ℝ), 0 ≤ C' ∧ ∀ t ∈ Set.Ioo tη 0, cutoffEnstrophy χ u t + 1 ≤ C' * (-t) ^ (-(Cstar * η))

theorem CIV.closure_enstrophy_decay_sixteenth_eta_of_exists_energy_inequality {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) (hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {tη Cη : ℝ} (htη : tη ∈ Set.Ioo (-1) 0) (hCη : 0 ≤ Cη) {G W : ℝ → ℝ} (hW0 : ∀ t ∈ Set.Ioo tη 0, 0 ≤ W t) (hex : ∃ (Cstar : ℝ), 1 ≤ Cstar ∧ (∀ t ∈ Set.Ioo tη 0, deriv (cutoffEnstrophy χ u) t + cutoffEnstrophyDissipation χ u t ≤ Cstar * (G t + W t ^ 2 + 1) * (cutoffEnstrophy χ u t + 1)) ∧ (∀ t ∈ Set.Ioo tη 0, G t ≤ 1 / (16 * Cstar) / -t) ∧ ∀ t ∈ Set.Ioo tη 0, W t ≤ Cη * (-t) ^ (-(1 / (16 * Cstar)))) : ∃ (C' : ℝ), 0 ≤ C' ∧ ∀ t ∈ Set.Ioo tη 0, cutoffEnstrophy χ u t + 1 ≤ C' * (-t) ^ (-(1 / 16))

theorem CIV.closure_enstrophy_decay_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)) {η Cη : ℝ} (hη : 0 < η ∧ 2 * η < 1) (hCη : 0 ≤ Cη) (hGη : ∀ t ∈ Set.Ioo tη 0, G t ≤ η / -t) (hW0 : ∀ t ∈ Set.Ioo tη 0, 0 ≤ W t) (hWη : ∀ t ∈ Set.Ioo tη 0, W t ≤ Cη * (-t) ^ (-η)) : ∃ (Cstar : ℝ), 1 ≤ Cstar ∧ ∃ (C' : ℝ), 0 ≤ C' ∧ ∀ t ∈ Set.Ioo tη 0, cutoffEnstrophy χ u t + 1 ≤ C' * (-t) ^ (-(Cstar * η))