Phase-shifted half-space weight

Factoring out the fixed normal phase leaves a tangential Gaussian and an exponential that decays on the cutoff transition region.

noncomputable def ESS.buShortShiftedWeight (scale a : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The half-space Carleman density with the fixed normal phase removed.

Equations

• ESS.buShortShiftedWeight scale a z = Real.exp (-(2 * a * ESS.buShortB scale)) * ESS.buShortCarlemanWeight a z

theorem ESS.buShortShiftedWeight_eq (scale a : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (htime : 0 < z.2) : buShortShiftedWeight scale a z = z.2 ^ 2 * Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * Real.exp (2 * a * (buShortF (z.1 2) z.2 - buShortB scale))

The phase-shifted weight separates into time, tangential Gaussian, and normal phase factors.

theorem ESS.buShortShiftedWeight_le_gap (scale a : ℝ) (ha : 0 ≤ a) (z : CKN.Foundation.Parabolic.ParabolicPoint) (htime : 0 < z.2) (htime1 : z.2 ≤ 1) (hgap : buShortF (z.1 2) z.2 - buShortB scale ≤ -buShortD scale / 2) : buShortShiftedWeight scale a z ≤ Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * Real.exp (-(a * buShortD scale))

Above the initial time and below time one, the shifted weight has the exponential phase gap bound.