Normalized dyadic cells

The shifted dyadic cell lies inside the local energy cylinder for the rescaled field.

theorem ESS.bu_short_dyadic_cell_normalized_inner (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.Foundation.buSmallTimeDyadicCell k m ell) : have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2; have r := √δ / 8; (z.1, 1 / 2 + z.2) ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y r) (Set.Ioo (1 / 2 + δ - r ^ 2 / 2) (1 / 2 + δ - r ^ 2 / 2 + r ^ 2))

A shifted short-time dyadic cell lies inside the inner local energy cylinder at its midpoint (lem:bu-small-time).