Dyadic cells in Gaussian averaging boxes

The Gaussian averaging box at each dyadic midpoint contains the corresponding shifted space-time cell.

theorem ESS.bu_short_shifted_dyadic_cell_average (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) : have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2; buShortShiftedDyadicCell k m ell ⊆ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2)) (Set.Ioo (1 / 2 + δ / 2) (1 / 2 + 5 * δ / 4))

The shifted dyadic cell is contained in the Gaussian averaging box at its center (lem:bu-small-time).