Weighted factors on short-time cells

The tangential Gaussian, fourth-order normal factor, and fixed normal phase are controlled by a Gaussian at the dyadic cell midpoint.

theorem ESS.bu_short_weighted_cell_factor_bound (scale a b : ℝ) (hscale : 0 < scale) (ha : 0 ≤ a) (hb : 0 < b) : ∃ (C : ℝ), 0 < C ∧ ∀ (k : ℤ), 0 ≤ k → ∀ (m : Fin 3 → ℤ) (ell : Fin 2048), ∀ z ∈ buShortShiftedDyadicCell k m ell, z ∈ buShortHighStrip scale → have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * (1 + z.1 2) ^ 4 * Real.exp (2 * a * (buShortF (z.1 2) z.2 - buShortB scale)) ≤ C * Real.exp (-(Y 0 ^ 2 + Y 1 ^ 2) / 8) * Real.exp (b * Y 2 ^ 2)

All fixed short-time weight factors on a high-strip cell are bounded by a center Gaussian and an arbitrarily weak normal quadratic exponential (lem:bu-small-time).