Regional short-time summability

Cell bounds on a measurable subregion of the short-time slab imply integrability on that subregion.

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

Gaussian cell bounds restricted to a measurable short-time region imply integrability there (lem:bu-small-time).