Cell-center Gaussians on the integer lattice #

The dyadic spatial midpoint has a coordinate square proportional to the dyadic scale and a half-integer square.

theorem ESS.bu_short_dyadic_center_coordinate_sq (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) (i : Fin 3) :

Squared coordinates of a dyadic spatial midpoint.

theorem ESS.bu_short_center_gaussian_le_lattice_profile (β : ℝ) (hβ : 0 < β) (k : ℤ) (hk : 0 ≤ k) (m : Fin 3 → ℤ) (ell : Fin 2048) :

have d := CKN.Foundation.buSmallTimeDyadicScale k; have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; have a := 1 / (16 * 16384); have b := β / (48 * 16384); have K := (Real.exp (a / 4) * (a + 2) / a) ^ 2 * (Real.exp (b / 4) * (1 + 2 / b)); Real.exp (-(Y 0 ^ 2 + Y 1 ^ 2) / 16) * Real.exp (-(β * Y 2 ^ 2 / (48 * d))) ≤ K / d ^ 2 * buShortSpatialProfile m

The remaining cell-center Gaussian is bounded by a fixed summable lattice profile with two inverse dyadic powers.

Documentation