Integrability on the short normalized slab

The abstract dyadic cell estimate controls integration on the full short-time slab because the cells cover it almost everywhere.

theorem ESS.bu_short_integrable_on_short_slab (N : ℕ) (c K : ℝ) (hc : 0 < c) (F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hCellInt : ∀ (k : ℕ) (m : Fin 3 → ℤ) (ell : Fin 2048), MeasureTheory.IntegrableOn F (buShortShiftedDyadicCell (↑k + 1) m ell) MeasureTheory.volume) (hCellBound : ∀ (k : ℕ) (m : Fin 3 → ℤ) (ell : Fin 2048), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in buShortShiftedDyadicCell (↑k + 1) m ell, ‖F z‖ ≤ K * (2 ^ (N * (k + 1)) * Real.exp (-(c * 2 ^ (k + 1)))) * buShortSpatialProfile m) : MeasureTheory.IntegrableOn F (Set.univ ×ˢ Set.Ioo (1 / 2) 1) MeasureTheory.volume

Polynomially weighted Gaussian cell bounds imply integrability on the short-time slab (lem:bu-small-time).