OAI/NumberTheory/CubicMoment/Estimates/PrincipalLatticeTheta.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Poisson inversion of the principal lattice Gaussian, with its zero term retained. This supplies the pole term of the principal ideal zeta function rather than treating it as a nonprincipal Hecke function.

  1. def OAI.CubicFirstMoment.principalLatticeTheta line 11
  2. lemma OAI.CubicFirstMoment.principalLatticeTheta_inversion line 14