Dyadic Gaussian decay

Any fixed polynomial factor in the dyadic index is dominated by the normal Gaussian decay used in lem:bu-small-time.

theorem ESS.bu_short_dyadic_gaussian_summable (N : ℕ) (c : ℝ) (hc : 0 < c) : Summable fun (k : ℕ) => 2 ^ (N * k) * Real.exp (-(c * 2 ^ k))

A polynomial in the dyadic spatial scale times a normal Gaussian tail is summable (lem:bu-small-time).