OAI/NumberTheory/CubicMoment/Estimates/IdealThetaCompletion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Analytic continuation from the exact ideal theta transformation. The hypotheses concern the theta series itself and follow from the finite-character Poisson formula.

  1. def OAI.CubicFirstMoment.idealThetaFEPair line 13
  2. lemma OAI.CubicFirstMoment.idealThetaFEPair_strong line 33
  3. lemma OAI.CubicFirstMoment.thetaHeckeL_eq_series line 41
  4. lemma OAI.CubicFirstMoment.idealThetaFEPair_hecke line 52