OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeValuationSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The literal lower-chart sum split into its three exact prime valuations and its zero class. All reductions preserve the sharp modulus.

  1. lemma OAI.CubicFirstMoment.cubicThetaResiduesOne_tsum line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubePeriodic_sum line 16
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeLowerValue_sum line 66