Cutoff Enstrophy Balance Annulus Bound

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.isClosed_closedAnnulus (Rm' Rp' : ℝ) : IsClosed {x : CKN.Foundation.Parabolic.Vec3 | Rm' ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm x ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ Rp'}

The closed annulus {x | Rm' ≤ ‖x‖ ∧ ‖x‖ ≤ Rp'} is closed in the Euclidean topology on Vec3.

theorem CIV.cutoff_enstrophy_balance_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) (hMf : ForceC2Bounded f) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) (hχU : tsupport χ ⊆ 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 M : ℝ} (hM : 0 ≤ M) (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)| ≤ M) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Ioo t₀ 0, HasDerivAt (cutoffEnstrophy χ u) (deriv (cutoffEnstrophy χ u) t) t ∧ 1 / 2 * deriv (cutoffEnstrophy χ u) t + cutoffEnstrophyDissipation χ u t ≤ cutoffStretching χ u t + C * (cutoffEnstrophy χ u t + 1)

When the velocity u and its vorticity satisfy a uniform order-≤2 multiPartial bound on the open annulus Rm < ‖x‖ < Rp, the tested enstrophy balance eq:aniso:closure:tested holds on any closed subset A of that annulus, with Mu = M and Mω = 2M. This bridges lem:aniso:annulus's open-annulus multi-index bound to cutoff_enstrophy_balance's closed-set velocity/vorticity hypotheses hubd/hωbd.

theorem CIV.cutoff_enstrophy_balance_of_multiPartial_le_closedAnnulus {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) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) (hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (-1) 0) {Rm Rm' Rp' Rp M : ℝ} (hM : 0 ≤ M) (hRm : Rm < Rm') (hRp : Rp' < Rp) (hχA : ∀ x ∉ {x : CKN.Foundation.Parabolic.Vec3 | Rm' ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm x ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ Rp'}, fderiv ℝ χ x = 0) (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)| ≤ M) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Ioo t₀ 0, HasDerivAt (cutoffEnstrophy χ u) (deriv (cutoffEnstrophy χ u) t) t ∧ 1 / 2 * deriv (cutoffEnstrophy χ u) t + cutoffEnstrophyDissipation χ u t ≤ cutoffStretching χ u t + C * (cutoffEnstrophy χ u t + 1)

The concrete closed sub-annulus Rm' ≤ ‖x‖ ≤ Rp' (with Rm < Rm' ≤ Rp' < Rp) is contained in the open annulus Rm < ‖x‖ < Rp, so the hypotheses of cutoff_enstrophy_balance_of_multiPartial_le are satisfied. This is the instance needed when a cutoff's gradient support occupies a closed annulus.