Tangential Gaussian on dyadic cells

The tangential Gaussian at any cell point is controlled by a slightly weaker Gaussian at the spatial midpoint.

theorem ESS.bu_short_tangential_cell_weight_le (k : ℤ) (hk : 0 ≤ k) (m : Fin 3 → ℤ) (ell : Fin 2048) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ buShortShiftedDyadicCell k m ell) (hs : z.2 ∈ Set.Ioo (1 / 2) 1) : have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) ≤ Real.exp 1 * Real.exp (-(Y 0 ^ 2 + Y 1 ^ 2) / 8)

A dyadic cell's tangential Gaussian is bounded by its center Gaussian with half the quadratic exponent (lem:bu-small-time).