The shifted half-space weight

At exponent three quarters the half-space Carleman phase splits into a tangential Gaussian and the normal phase used in lem:bu-small-time.

theorem ESS.bu_halfSpacePhase_eq (a : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (htime : 0 < z.2) : halfSpacePhase a (3 / 4) z = -(z.1 0 ^ 2 + z.1 1 ^ 2) / (8 * z.2) + a * buShortF (z.1 2) z.2

The half-space phase at exponent three quarters is a tangential Gaussian plus a times the normal phase.

theorem ESS.bu_halfSpaceWeight_split (a scale : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (htime : 0 < z.2) : Real.exp (2 * halfSpacePhase a (3 / 4) z) = Real.exp (2 * a * buShortB scale) * (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)))

Factoring out the fixed phase shift changes the exponential weight only by a constant independent of space and time.