OAI/NumberTheory/CubicMoment/Estimates/PrincipalIdealTheta.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The principal theta function includes the zero vector. Its exact unit multiplicity gives the inhomogeneous transformation of the ideal theta sum and therefore the principal zeta pole.

  1. lemma OAI.CubicFirstMoment.principalIdealTheta_nonzero line 12
  2. lemma OAI.CubicFirstMoment.principalLatticeTheta_summable line 32
  3. lemma OAI.CubicFirstMoment.principalLatticeTheta_eq_ideal line 46
  4. theorem OAI.CubicFirstMoment.principalIdealTheta_inversion line 66