Smooth localization inside a parabolic ball

A ball compactly inside the space-time domain admits a smooth cutoff and a compactly interior product box containing its support.

theorem CKN.Core.Endgame.localBox_of_parabolic_ball {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {z₀ : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hball : Metric.ball z₀ (2 * r) ⊆ spaceTimeSet Ω I) : localBox Ω I (Foundation.Parabolic.vec3Ball z₀.1 r) (Set.Ioo (z₀.2 - r ^ 2) (z₀.2 + r ^ 2))

A positive interior parabolic ball supplies a compactly interior spatial ball and time interval.

theorem CKN.Core.Endgame.exists_localization_cutoff {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {z₀ : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hball : Metric.ball z₀ (2 * r) ⊆ spaceTimeSet Ω I) : ∃ φ ∈ spaceTimeTestFunction Ω I, (∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ φ z ∧ φ z ≤ 1) ∧ (∀ z ∈ Metric.closedBall z₀ (r / 8), φ (z.1, z.2) = 1) ∧ tsupport φ ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ (r / 4) ∧ localBox Ω I (Foundation.Parabolic.vec3Ball z₀.1 r) (Set.Ioo (z₀.2 - r ^ 2) (z₀.2 + r ^ 2)) ∧ tsupport φ ⊆ Foundation.Parabolic.vec3Ball z₀.1 r ×ˢ Set.Ioo (z₀.2 - r ^ 2) (z₀.2 + r ^ 2)

There is a smooth cutoff equal to one on the closed ball of radius r/8, supported inside the ball of radius r/4, with a local product box containing its support.