The annulus-confined cutoff of lem:aniso:closure

The closure argument tests the vorticity equation against a cutoff χ that is 1 on an inner ball B(ρ) and supported in B(Rstar), so that ∇χ is carried by the closed annulus {ρ ≤ |x| ≤ Rstar}. Every consumer of the tested enstrophy balance eq:aniso:closure:tested asks for a closed set A carrying fderiv χ and contained in the open annulus {Rlo < |x| < Rhi} on which lem:aniso:annulus bounds the velocity; a cutoff that is 1 at the origin can never have A be a ball, so the closed annulus is the only shape that fits.

CKN.canonicalBallCutoff 0 ρ Rstar is such a cutoff: its derivative vanishes on the inner ball, where it is constantly 1, and off B(Rstar), where it vanishes on a neighbourhood of every point; what is left is exactly the closed annulus. Since χ 0 = 1, the data below is not the degenerate χ ≡ 0, which satisfies every clause about fderiv χ.

theorem CIV.fderiv_canonicalBallCutoff_eq_zero_of_notMem_closedAnnulus {ρ Rstar : ℝ} (hρ : 0 < ρ) (hρR : ρ < Rstar) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ {y : CKN.Foundation.Parabolic.Vec3 | ρ ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm y ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm y ≤ Rstar}) : fderiv ℝ (CKN.canonicalBallCutoff 0 ρ Rstar) x = 0

Outside the closed annulus {ρ ≤ |x| ≤ Rstar} the canonical ball cutoff has vanishing derivative: on the inner ball it is constantly 1, and beyond B(Rstar) it is constantly 0 on a neighbourhood.

theorem CIV.canonicalBallCutoff_zero_eq_one {ρ Rstar : ℝ} (hρ : 0 < ρ) (hρR : ρ < Rstar) : CKN.canonicalBallCutoff 0 ρ Rstar 0 = 1

The canonical ball cutoff takes the value 1 at the centre of its inner ball.

theorem CIV.canonicalBallCutoff_closedAnnulus_data {ρ Rstar : ℝ} (hρ : 0 < ρ) (hρR : ρ < Rstar) : ContDiff ℝ (↑⊤) (CKN.canonicalBallCutoff 0 ρ Rstar) ∧ HasCompactSupport (CKN.canonicalBallCutoff 0 ρ Rstar) ∧ tsupport (CKN.canonicalBallCutoff 0 ρ Rstar) ⊆ CKN.Foundation.Parabolic.vec3Ball 0 Rstar ∧ (∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ, CKN.canonicalBallCutoff 0 ρ Rstar x = 1) ∧ IsClosed {y : CKN.Foundation.Parabolic.Vec3 | ρ ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm y ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm y ≤ Rstar} ∧ (∀ x ∉ {y : CKN.Foundation.Parabolic.Vec3 | ρ ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm y ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm y ≤ Rstar}, fderiv ℝ (CKN.canonicalBallCutoff 0 ρ Rstar) x = 0) ∧ CKN.canonicalBallCutoff 0 ρ Rstar 0 = 1

The cutoff data of lem:aniso:closure's energy setup, with ∇χ confined to the closed annulus {ρ ≤ |x| ≤ Rstar}: the canonical ball cutoff is smooth and compactly supported inside B(Rstar), equals 1 on the inner ball B(ρ) — hence at the origin, so it is not identically zero — and its derivative vanishes off that closed annulus.

theorem CIV.cutoff_enstrophy_balance_canonicalBallCutoff {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) {ρ Rstar Rlo Rhi M : ℝ} (hρ : 0 < ρ) (hρR : ρ < Rstar) (hR1 : Rstar ≤ 1) (hRlo : Rlo < ρ) (hRhi : Rstar < Rhi) (hM : 0 ≤ M) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (-1) 0) (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rlo < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rhi → ∀ 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 (CKN.canonicalBallCutoff 0 ρ Rstar) u) (deriv (cutoffEnstrophy (CKN.canonicalBallCutoff 0 ρ Rstar) u) t) t ∧ 1 / 2 * deriv (cutoffEnstrophy (CKN.canonicalBallCutoff 0 ρ Rstar) u) t + cutoffEnstrophyDissipation (CKN.canonicalBallCutoff 0 ρ Rstar) u t ≤ cutoffStretching (CKN.canonicalBallCutoff 0 ρ Rstar) u t + C * (cutoffEnstrophy (CKN.canonicalBallCutoff 0 ρ Rstar) u t + 1)

The tested enstrophy balance eq:aniso:closure:tested for the canonical ball cutoff. With radii Rlo < ρ < Rstar < Rhi and Rstar ≤ 1, the gradient of CKN.canonicalBallCutoff 0 ρ Rstar is carried by the closed annulus {ρ ≤ |x| ≤ Rstar}, which sits inside the open annulus {Rlo < |x| < Rhi} of lem:aniso:annulus. The order-≤ 2 velocity bound there therefore discharges the pointwise velocity and vorticity hypotheses of cutoff_enstrophy_balance, and the balance holds for a cutoff that is 1 on B(ρ).