Annulus Bounds Enstrophy

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

theorem CIV.abs_apply_and_vorticityField_le_of_multiPartial_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Rm Rp t₀ M : ℝ} (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) (hM : 0 ≤ M) (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), |u (x, t) i| ≤ M ∧ |vorticityField u (x, t) i| ≤ 2 * M

The second-order derivative bound supplied by lem:aniso:annulus on the regular annulus reduces to pointwise bounds on the velocity u and the vorticity vorticityField u: |u_i| ≤ M and |ω_i| ≤ 2M whenever the multi-index bound hbound holds on the annulus Rm < ‖x‖ < Rp. This is the translation that cutoff_enstrophy_balance needs to connect the closed-set hypothesis it receives to the open-annulus hypothesis lem:aniso:annulus provides.