A summable integer lattice profile

A fixed reciprocal-square profile dominates half-integer Gaussians with an explicit inverse-width factor.

noncomputable def ESS.buShortIntProfile (n : ℤ) : ℝ

Reciprocal-square lattice profile, normalized at the origin.

Equations

• ESS.buShortIntProfile n = if n = 0 then 1 else 1 / ↑n ^ 2

theorem ESS.bu_short_int_profile_summable : Summable buShortIntProfile

The reciprocal-square lattice profile is summable.

theorem ESS.bu_short_int_profile_nonneg (n : ℤ) : 0 ≤ buShortIntProfile n

The reciprocal-square lattice profile is nonnegative.

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

A half-integer Gaussian is bounded by a fixed summable profile with one inverse power of its width (lem:bu-small-time).