The three short-time density factors on a cell

Each factor multiplying rescaled quadratic energy is bounded by a common center Gaussian.

theorem ESS.bu_short_three_cell_factors_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; have Bound := C * Real.exp (-(Y 0 ^ 2 + Y 1 ^ 2) / 8) * Real.exp (b * Y 2 ^ 2); Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * (1 + z.1 2) ^ 4 ≤ Bound ∧ buShortShiftedWeight scale a z * (1 + z.1 2) ^ 4 ≤ Bound ∧ buShortShiftedWeight scale a z ≤ Bound

The tangential factor and both shifted Carleman factors share a center Gaussian bound on the high normal strip (lem:bu-small-time).