Time cutoffs for Gaussian unique continuation

The upper cutoff turns off before time 7/4. The lower cutoff turns on between times ε and 2ε.

noncomputable def ESS.ucFinalTimeCutoff (s : ℝ) : ℝ

The final-time cutoff in lem:uc-gaussian.

Equations

• ESS.ucFinalTimeCutoff s = CKN.smoothTransitionProfile (7 - 4 * s)

noncomputable def ESS.ucInitialTimeCutoff (ε s : ℝ) : ℝ

The initial-time cutoff in lem:uc-gaussian.

Equations

• ESS.ucInitialTimeCutoff ε s = CKN.smoothTransitionProfile ((s - ε) / ε)

theorem ESS.ucFinalTimeCutoff_smooth : ContDiff ℝ (↑⊤) ucFinalTimeCutoff

The final-time cutoff is smooth.

theorem ESS.ucInitialTimeCutoff_smooth (ε : ℝ) : ContDiff ℝ (↑⊤) (ucInitialTimeCutoff ε)

The initial-time cutoff is smooth in the time variable.

theorem ESS.ucFinalTimeCutoff_eq_one {s : ℝ} (hs : s ≤ 3 / 2) : ucFinalTimeCutoff s = 1

The final-time cutoff equals one before time 3/2.

theorem ESS.ucFinalTimeCutoff_eq_zero {s : ℝ} (hs : 7 / 4 ≤ s) : ucFinalTimeCutoff s = 0

The final-time cutoff vanishes from time 7/4 onward.

theorem ESS.ucInitialTimeCutoff_eq_zero {ε s : ℝ} (hε : 0 < ε) (hs : s ≤ ε) : ucInitialTimeCutoff ε s = 0

The initial-time cutoff vanishes through time ε.

theorem ESS.ucInitialTimeCutoff_eq_one {ε s : ℝ} (hε : 0 < ε) (hs : 2 * ε ≤ s) : ucInitialTimeCutoff ε s = 1

The initial-time cutoff equals one from time 2ε onward.

theorem ESS.ucFinalTimeCutoff_bounds (s : ℝ) : 0 ≤ ucFinalTimeCutoff s ∧ ucFinalTimeCutoff s ≤ 1

The final-time cutoff takes values between zero and one.

theorem ESS.ucInitialTimeCutoff_bounds (ε s : ℝ) : 0 ≤ ucInitialTimeCutoff ε s ∧ ucInitialTimeCutoff ε s ≤ 1

The initial-time cutoff takes values between zero and one.

theorem ESS.ucFinalTimeCutoff_abs_deriv_le (s : ℝ) : |deriv ucFinalTimeCutoff s| ≤ 32

The final-time cutoff has an absolute first-derivative bound.

theorem ESS.ucInitialTimeCutoff_abs_deriv_le {ε : ℝ} (hε : 0 < ε) (s : ℝ) : |deriv (ucInitialTimeCutoff ε) s| ≤ 8 / ε

The initial-time cutoff has derivative at most 8/ε in absolute value.