From Gaussian averages to summable cell bounds

The local energy estimate and Gaussian average produce the dyadic normal tail required for summing all short-time cells.

theorem ESS.bu_short_cell_average_algebra (β G b Cw Ce Cg I Avg : ℝ) (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) (hI : I ≤ have d := CKN.Foundation.buSmallTimeDyadicScale k; have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; Cw * Real.exp (-(Y 0 ^ 2 + Y 1 ^ 2) / 8) * Real.exp (b * Y 2 ^ 2) * (Ce / d) * Avg) (hAvg : Avg ≤ have d := CKN.Foundation.buSmallTimeDyadicScale k; have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; Cg * d ^ 2 * Real.exp (G * (Y 0 ^ 2 + Y 1 ^ 2 + Y 2 ^ 2)) * Real.exp (-(β * Y 2 ^ 2 / (12 * d)))) : have d := CKN.Foundation.buSmallTimeDyadicScale k; 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₀)); I ≤ Cw * Ce * Cg * K₀ / d * Real.exp (-(β / (12 * d))) * buShortSpatialProfile m

A cell integral bounded by its Gaussian velocity average has a summable lattice majorant (lem:bu-small-time).