Spatial cutoff for Gaussian unique continuation

The canonical smooth ball cutoff has a unit-width transition collar when the normalized cylinder radius is at least four.

noncomputable def ESS.ucSpatialCutoff (ρ : ℝ) (hρ : 0 < ρ) : CKN.Foundation.Parabolic.Vec3 → ℝ

The spatial cutoff in lem:uc-gaussian.

Equations

• ESS.ucSpatialCutoff ρ hρ = CKN.mollifiedBallCutoff 0 hρ

theorem ESS.ucSpatialCutoff_smooth {ρ : ℝ} (hρ : 0 < ρ) : ContDiff ℝ (↑⊤) (ucSpatialCutoff ρ hρ)

The spatial cutoff is smooth for normalized radii at least four.

theorem ESS.ucSpatialCutoff_eq_one {ρ : ℝ} (hρ : 0 < ρ) {y : CKN.Foundation.Parabolic.Vec3} (hy : y ∈ CKN.Foundation.Parabolic.vec3Ball 0 (ρ / 2)) : ucSpatialCutoff ρ hρ y = 1

The spatial cutoff equals one on the inner ball.

theorem ESS.ucSpatialCutoff_tsupport {ρ : ℝ} (hρ : 0 < ρ) : tsupport (ucSpatialCutoff ρ hρ) ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ

The topological support of the spatial cutoff is inside the outer ball.

theorem ESS.ucSpatialCutoff_bounds {ρ : ℝ} (hρ : 0 < ρ) (y : CKN.Foundation.Parabolic.Vec3) : 0 ≤ ucSpatialCutoff ρ hρ y ∧ ucSpatialCutoff ρ hρ y ≤ 1

The spatial cutoff takes values between zero and one.

theorem ESS.ucSpatialCutoff_spatialPartial_bound {ρ : ℝ} (hρ : 0 < ρ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (j : Fin 3) : |CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ q.1) j z| ≤ CKN.cutoffGradientConstant / ρ

Each coordinate derivative of the spatial cutoff has a uniform bound.

theorem ESS.ucSpatialCutoff_spatialSecondPartial_bound {ρ : ℝ} (hρ : 0 < ρ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) : |CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff ρ hρ q.1) i j z| ≤ CKN.cutoffSecondDerivativeConstant / ρ ^ 2

The spatial cutoff has a second derivative bound given by the fixed CKN cutoff constant.