Support and smoothness of a cutoff's spatial multi-index derivatives

The ball cutoff serrinBallCutoff x ρ, lifted to a time-independent function of ParabolicPoint, is constant (1 near x, 0 past radius ρ) on the two open sets flanking the annulus ρ/2 ≤ |y - x| ≤ ρ, so every nonzero spatial multi-index derivative of it vanishes there and is supported in that compact annulus; every such derivative, including the zeroth, is globally smooth. These are the facts that make the cutoff-times-kernel product in the interior estimates of lem:aniso:annulus a smooth, compactly supported function away from the Newtonian kernel's singularity, ready for integration by parts.

Part 1: peeling one derivative off a multi-index

theorem CIV.multiPartial_peel {γ : Fin 3 → ℕ} (hγ : γ 0 + γ 1 + γ 2 ≠ 0) (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : ∃ (j : Fin 3) (γ' : Fin 3 → ℕ), γ' 0 + γ' 1 + γ' 2 + 1 = γ 0 + γ 1 + γ 2 ∧ multiPartial g γ = CKN.spatialPartial (multiPartial g γ') j

A nonzero spatial multi-index derivative peels one derivative off the outermost nonvanishing exponent.

Part 2: the cutoff's derivatives vanish off the annulus

Part 3: compact support of a nonzero cutoff derivative

theorem CIV.support_multiPartial_cutoff_subset {x : CKN.Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {γ : Fin 3 → ℕ} (hγ : γ 0 + γ 1 + γ 2 ≠ 0) (t : ℝ) : (Function.support fun (y : CKN.Foundation.Parabolic.Vec3) => multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinBallCutoff x ρ z.1) γ (y, t)) ⊆ {y : CKN.Foundation.Parabolic.Vec3 | ρ / 2 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ}

A nonzero derivative of the lifted cutoff is supported in the closed annulus ρ/2 ≤ |y - x| ≤ ρ.

theorem CIV.isCompact_cutoffAnnulus {x : CKN.Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) : IsCompact {y : CKN.Foundation.Parabolic.Vec3 | ρ / 2 ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ}

The compact annulus that carries a nonzero cutoff derivative.

theorem CIV.hasCompactSupport_multiPartial_cutoff {x : CKN.Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {γ : Fin 3 → ℕ} (hγ : γ 0 + γ 1 + γ 2 ≠ 0) (t : ℝ) : HasCompactSupport fun (y : CKN.Foundation.Parabolic.Vec3) => multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinBallCutoff x ρ z.1) γ (y, t)

A nonzero derivative of the lifted cutoff has compact support.

Part 4: global smoothness of a cutoff derivative

theorem CIV.contDiff_multiPartial_cutoff (x : CKN.Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (γ : Fin 3 → ℕ) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : CKN.Foundation.Parabolic.Vec3) => multiPartial (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinBallCutoff x ρ z.1) γ (y, t)

Every spatial multi-index derivative of the lifted cutoff is smooth.