Support of the Gaussian cutoff

The product cutoff in lem:uc-gaussian is smooth, compactly supported inside the normalized cylinder, and equals one on the inner box after its initial transition.

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

The scalar cutoff used in the Gaussian unique-continuation estimate.

Equations

• ESS.ucGaussianCutoff ρ hρ ε = ESS.ucCutoffScalar (ESS.ucSpatialCutoff ρ hρ) ESS.ucFinalTimeCutoff (ESS.ucInitialTimeCutoff ε)

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

The Gaussian scalar cutoff is smooth.

theorem ESS.ucGaussianCutoff_support_subset {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) : Function.support (ucGaussianCutoff ρ hρ ε) ⊆ CKN.euclideanClosedBall 0 (3 * ρ / 4) ×ˢ Set.Icc ε (7 / 4)

The support of the Gaussian scalar cutoff lies in a fixed compact spatial ball and a closed positive-time interval.

theorem ESS.ucGaussianCutoff_hasCompactSupport {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) : HasCompactSupport (ucGaussianCutoff ρ hρ ε)

The Gaussian cutoff has compact support.

theorem ESS.ucGaussianCutoff_tsupport_subset_cylinder {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) : tsupport (ucGaussianCutoff ρ hρ ε) ⊆ ucCylinder ρ

The topological support stays strictly inside the positive-time normalized cylinder.

theorem ESS.ucGaussianCutoff_eq_one_on_inner {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ ucInnerRegion ρ) (hs : 2 * ε ≤ z.2) : ucGaussianCutoff ρ hρ ε z = 1

The Gaussian cutoff equals one on the interior after the initial-time transition.

theorem ESS.ucGaussianCutoff_bounds {ρ : ℝ} (hρ : 0 < ρ) (ε : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : 0 ≤ ucGaussianCutoff ρ hρ ε z ∧ ucGaussianCutoff ρ hρ ε z ≤ 1

The Gaussian cutoff takes values between zero and one.