Geometry of the short-time dyadic cells

Each time cell lies close to its center. This permits one Gaussian average and one Caccioppoli estimate to control its quadratic energy in lem:bu-small-time.

theorem ESS.bu_short_dyadic_cell_time_distance_le (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.Foundation.buSmallTimeDyadicCell k m ell) : |z.2 - (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2| ≤ CKN.Foundation.buSmallTimeDyadicTimeLength k / 2

Time coordinates in a dyadic cell differ from the midpoint by at most half the time-cell length.

theorem ESS.bu_short_dyadic_cell_center_time_bounds (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) : CKN.Foundation.buSmallTimeDyadicScale k / 2 < (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 ∧ (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2 < CKN.Foundation.buSmallTimeDyadicScale k

The dyadic midpoint time lies in the same layer as its cell.