Summing the short-time cells

The normal Gaussian decay dominates any fixed dyadic polynomial, while a reciprocal-square profile sums the spatial grid.

theorem ESS.bu_short_shifted_dyadic_gaussian_summable (N : ℕ) (c : ℝ) (hc : 0 < c) : Summable fun (k : ℕ) => 2 ^ (N * (k + 1)) * Real.exp (-(c * 2 ^ (k + 1)))

A fixed dyadic polynomial times normal Gaussian decay remains summable after shifting the index to the short-time layers.

theorem ESS.bu_short_integrable_on_shifted_dyadic_cells (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 (⋃ (ij : (ℕ × (Fin 3 → ℤ)) × Fin 2048), buShortShiftedDyadicCell (↑ij.1.1 + 1) ij.1.2 ij.2) MeasureTheory.volume

A Gaussian cell estimate with any fixed dyadic polynomial implies integrability on the union of shifted cells (lem:bu-small-time).