OAI/NumberTheory/CubicMoment/Estimates/ResidueHeckeFromFourier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The primitive Hecke completion constructed from the finite Gauss Fourier computation. This bridge assumes no analytic continuation or growth result.

  1. lemma OAI.CubicFirstMoment.residueLatticeTheta_inversion_from_fourier line 11
  2. lemma OAI.CubicFirstMoment.residueHecke_from_finiteFourier line 28