Reciprocal dyadic scale

At the shifted short-time layer indexed by k + 1, the reciprocal scale is the corresponding positive power of two.

theorem ESS.bu_short_dyadic_scale_reciprocal (k : ℕ) : (CKN.Foundation.buSmallTimeDyadicScale (↑k + 1))⁻¹ = 2 ^ (k + 1)

The reciprocal of a short-time dyadic scale is a natural power of two (lem:bu-small-time).

theorem ESS.bu_short_dyadic_tail_rewrite (β K P : ℝ) (k : ℕ) : K / CKN.Foundation.buSmallTimeDyadicScale (↑k + 1) * Real.exp (-(β / (12 * CKN.Foundation.buSmallTimeDyadicScale (↑k + 1)))) * P = K * (2 ^ (k + 1) * Real.exp (-(β / 12 * 2 ^ (k + 1)))) * P

A single inverse dyadic power and its Gaussian tail have the summable form used by the cell partition (lem:bu-small-time).