Coverage by shifted dyadic layers

The shifted layers cover the short normalized time interval, apart from their measure-zero upper endpoints.

theorem ESS.bu_short_natural_dyadic_scale (k : ℕ) : CKN.Foundation.buSmallTimeDyadicScale (↑k + 1) = (1 / 2) ^ (k + 1)

The integer-indexed dyadic scale equals a natural power of one half.

theorem ESS.bu_short_shifted_ioc_layers_cover : ⋃ (k : ℕ), Set.Ioc (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale (↑k + 1) / 2) (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale (↑k + 1)) = Set.Ioc (1 / 2) 1

The half-open shifted dyadic layers cover the half-open normalized time interval.

theorem ESS.bu_short_shifted_open_layers_ae : ⋃ (k : ℕ), Set.Ioo (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale (↑k + 1) / 2) (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale (↑k + 1)) =ᵐ[MeasureTheory.volume] Set.Ioo (1 / 2) 1

The open shifted dyadic layers cover normalized time up to null endpoints.

theorem ESS.bu_short_shifted_parabolic_layers_ae : ⋃ (k : ℕ), Set.univ ×ˢ Set.Ioo (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale (↑k + 1) / 2) (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale (↑k + 1)) =ᵐ[MeasureTheory.volume] Set.univ ×ˢ Set.Ioo (1 / 2) 1

The shifted dyadic space-time layers cover the short normalized slab up to a null set.