Algebra of a weighted cell bound

The dyadic average volume offsets the local energy and lattice costs, leaving one inverse dyadic factor and a normal Gaussian tail.

theorem ESS.bu_short_cell_gaussian_algebra (β G b Cw Ce Cg : ℝ) (hβ : 0 < β) (hGtan : G ≤ 1 / 16) (hGnorm : G ≤ β / 48) (hbβ : b ≤ β / 48) (hCw : 0 ≤ Cw) (hCe : 0 ≤ Ce) (hCg : 0 ≤ Cg) (k : ℤ) (hk : 1 ≤ k) (m : Fin 3 → ℤ) (ell : Fin 2048) (hY : 2 ≤ (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 2) : have d := CKN.Foundation.buSmallTimeDyadicScale k; have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; have a := 1 / (16 * 16384); have b₀ := β / (48 * 16384); have K₀ := (Real.exp (a / 4) * (a + 2) / a) ^ 2 * (Real.exp (b₀ / 4) * (1 + 2 / b₀)); Cw * Real.exp (-(Y 0 ^ 2 + Y 1 ^ 2) / 8) * Real.exp (b * Y 2 ^ 2) * (Ce / d) * (Cg * d ^ 2 * Real.exp (G * (Y 0 ^ 2 + Y 1 ^ 2 + Y 2 ^ 2)) * Real.exp (-(β * Y 2 ^ 2 / (12 * d)))) ≤ Cw * Ce * Cg * K₀ / d * Real.exp (-(β / (12 * d))) * buShortSpatialProfile m

The center Gaussian and dyadic factors have a summable common majorant (lem:bu-small-time).