A cutoff on the positive-time Gaussian cylinder

The initial transition is translated to the positive starting face in lem:bu-gaussian, so the Gaussian weight remains bounded on its support.

noncomputable def ESS.buGaussianShiftedCutoff (ρ : ℝ) (hρ : 0 < ρ) (ε : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The Gaussian cutoff shifted to start at time 1/6 and stopped before time 2. (lem:bu-gaussian#cutoff-construction).

Equations

• ESS.buGaussianShiftedCutoff ρ hρ ε z = ESS.ucGaussianCutoff ρ hρ ε ((ESS.buGaussianTimeShiftPoint (1 / 6)).symm z)

theorem ESS.buGaussian_shiftedCutoff_smooth (ρ : ℝ) (hρ : 0 < ρ) (ε : ℝ) : ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => buGaussianShiftedCutoff ρ hρ ε z

The scalar shifted cutoff is smooth.

theorem ESS.buGaussian_shiftedCutoff_hasCompactSupport {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) : HasCompactSupport (buGaussianShiftedCutoff ρ hρ ε)

The shifted cutoff has compact support.

theorem ESS.buGaussian_shiftedCutoff_tsupport_subset {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) : tsupport (buGaussianShiftedCutoff ρ hρ ε) ⊆ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2)

The topological support of the shifted cutoff lies in the positive-time Gaussian cylinder.