OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialRawVoronoi.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual radial raw/completed Voronoi identities. The main term remains in terms of the computed residue, without asserting its normalization.

  1. def OAI.CubicFirstMoment.cubicThetaActualRawRadialMain line 12
  2. def OAI.CubicFirstMoment.cubicThetaActualCompletedRadialMain line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaRadialGauss_ne_zero line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaRadialRawScalar_ne_zero line 28
  5. theorem OAI.CubicFirstMoment.cubicTheta_raw_radial_voronoi line 35
  6. lemma OAI.CubicFirstMoment.cubicTheta_radial_main_completed line 60
  7. theorem OAI.CubicFirstMoment.cubicTheta_completed_radial_voronoi line 71