OAI/NumberTheory/CubicMoment/Theta/CubicThetaVoronoiScale.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact frequency bookkeeping for the constructed transform. The common cusp numerator n represents n/lambda^4; the published dual argument represents n/lambda. The conversion is recorded without changing either normalization or identifying the two transform arguments.

  1. lemma OAI.CubicFirstMoment.cubicThetaFrequency_to_metaplectic line 12
  2. lemma OAI.CubicFirstMoment.cubicTheta_metaplectic_normSq line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaLevelScale_fourth line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaVoronoi_dual_argument line 30
  5. lemma OAI.CubicFirstMoment.cubicThetaVoronoi_dual_argument_ne_printed line 38