Extending the cutoff-times-slice product by zero

For a window B_bar(x, ρ) × [s - ρ², s] compactly contained in an open set O on which w is smooth, there is a globally smooth, compactly supported ζ agreeing with serrinCutoff x s ρ · w for every z with z.2 ≤ s. The construction multiplies w by an auxiliary cutoff equal to 1 on a slightly larger window, chosen (using a positive margin from the compactness of the window inside the open O) small enough that its support still lies in O; since serrinCutoff already vanishes off the window for z.2 ≤ s, the auxiliary cutoff's exact values elsewhere are immaterial. This is the extension-by-zero step of the proof of lem:aniso:annulus.

theorem CIV.HB2b_cutoff_extension {w : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {O : Set CKN.Foundation.Parabolic.ParabolicPoint} {x : CKN.Foundation.Parabolic.Vec3} {s ρ : ℝ} (hO : IsOpen O) (hρ : 0 < ρ) (hwin : {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} ×ˢ Set.Icc (s - ρ ^ 2) s ⊆ O) (hw : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => w z) O) : ∃ (ζ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ζ z) ∧ (HasCompactSupport fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ζ z) ∧ ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≤ s → ζ z = serrinCutoff x s ρ z * w z