A fixed summable spatial lattice profile

The product reciprocal-square profile dominates Gaussian cell-center weights at every dyadic scale.

noncomputable def ESS.buShortSpatialProfile (m : Fin 3 → ℤ) : ℝ

Product reciprocal-square profile on the three-dimensional grid.

Equations

• ESS.buShortSpatialProfile m = ESS.buShortIntProfile (m 0) * (ESS.buShortIntProfile (m 1) * ESS.buShortIntProfile (m 2))

theorem ESS.bu_short_spatial_profile_summable : Summable buShortSpatialProfile

The three-dimensional lattice profile is summable.

theorem ESS.bu_short_scaled_half_gaussian_le_profile (a d : ℝ) (ha : 0 < a) (hd : 0 < d) (hd1 : d ≤ 1) (n : ℤ) : Real.exp (-(a * d * (↑n + 1 / 2) ^ 2)) ≤ Real.exp (a / 4) * (a + 2) / (a * d) * buShortIntProfile n

A half-integer Gaussian with width proportional to a dyadic scale is controlled by the fixed profile and one inverse power of the scale.

theorem ESS.bu_short_separable_gaussian_le_profile (a b d : ℝ) (ha : 0 < a) (hb : 0 < b) (hd : 0 < d) (hd1 : d ≤ 1) (m : Fin 3 → ℤ) : Real.exp (-(a * d * (↑(m 0) + 1 / 2) ^ 2)) * (Real.exp (-(a * d * (↑(m 1) + 1 / 2) ^ 2)) * Real.exp (-(b * (↑(m 2) + 1 / 2) ^ 2))) ≤ (Real.exp (a / 4) * (a + 2) / (a * d)) ^ 2 * (Real.exp (b / 4) * (1 + 2 / b)) * buShortSpatialProfile m

A separable dyadic Gaussian on three grid coordinates is bounded by a fixed summable profile with a quadratic inverse-scale factor.