Shifted dyadic cells

The short-time grid is translated to the half-space Carleman time coordinate, which begins at one half.

theorem ESS.bu_short_time_shift_point_eval (q : CKN.Foundation.Parabolic.ParabolicPoint) : (buGaussianTimeShiftPoint (1 / 2)) q = (q.1, 1 / 2 + q.2)

Forward translation by one half in normalized time.

def ESS.buShortShiftedDyadicCell (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) : Set CKN.Foundation.Parabolic.ParabolicPoint

A dyadic cell translated forward by one half in time.

Equations

• ESS.buShortShiftedDyadicCell k m ell = ⇑(ESS.buGaussianTimeShiftPoint (1 / 2)) '' CKN.Foundation.buSmallTimeDyadicCell k m ell

theorem ESS.bu_short_shifted_dyadic_cell_inner (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) : have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2; have r := √δ / 8; buShortShiftedDyadicCell k m ell ⊆ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y r) (Set.Ioo (1 / 2 + δ - r ^ 2 / 2) (1 / 2 + δ - r ^ 2 / 2 + r ^ 2))

A shifted dyadic cell lies inside its local energy cylinder (lem:bu-small-time).