Almost-everywhere coverage by shifted cells

The shifted spatial and temporal grid covers each dyadic layer up to null time boundaries.

theorem ESS.bu_short_shifted_dyadic_cell_measurable (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) : MeasurableSet (buShortShiftedDyadicCell k m ell)

A shifted dyadic cell is measurable.

theorem ESS.bu_short_shifted_dyadic_cell_subset_layer (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) : buShortShiftedDyadicCell k m ell ⊆ Set.univ ×ˢ Set.Ioo (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale k / 2) (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale k)

Each shifted cell lies in its shifted dyadic time layer.

theorem ESS.bu_short_shifted_dyadic_cells_cover_ae (k : ℤ) : ⋃ (ij : (Fin 3 → ℤ) × Fin 2048), buShortShiftedDyadicCell k ij.1 ij.2 =ᵐ[MeasureTheory.volume] Set.univ ×ˢ Set.Ioo (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale k / 2) (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale k)

Shifted cells cover their dyadic layer almost everywhere.

theorem ESS.bu_short_shifted_all_cells_cover_ae : ⋃ (ij : (ℕ × (Fin 3 → ℤ)) × Fin 2048), buShortShiftedDyadicCell (↑ij.1.1 + 1) ij.1.2 ij.2 =ᵐ[MeasureTheory.volume] Set.univ ×ˢ Set.Ioo (1 / 2) 1

All shifted dyadic cells cover the short normalized slab almost everywhere (lem:bu-small-time).