Integration over shifted dyadic cells

Translation of the dyadic partition preserves parabolic measure.

theorem ESS.bu_short_shifted_dyadic_layer_image (k : ℤ) : ⇑(buGaussianTimeShiftPoint (1 / 2)) '' Set.univ ×ˢ Set.Ioo (CKN.Foundation.buSmallTimeDyadicScale k / 2) (CKN.Foundation.buSmallTimeDyadicScale k) = Set.univ ×ˢ Set.Ioo (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale k / 2) (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale k)

The time translation carries a dyadic layer to its shifted Carleman-time layer.

theorem ESS.bu_short_shifted_dyadic_layer_lintegral_eq_tsum (k : ℤ) (f : CKN.Foundation.Parabolic.ParabolicPoint → ENNReal) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in Set.univ ×ˢ Set.Ioo (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale k / 2) (1 / 2 + CKN.Foundation.buSmallTimeDyadicScale k), f z = ∑' (ij : (Fin 3 → ℤ) × Fin 2048), ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in buShortShiftedDyadicCell k ij.1 ij.2, f z

Nonnegative integration over a shifted dyadic layer equals the sum over its shifted cells (lem:bu-small-time).