OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticModelTorus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Continuous torus realization of the explicit arithmetic theta series. The nonconstant scalar is retained while its normalization is established.

  1. def OAI.CubicFirstMoment.cubicThetaArithmeticModelRemainder line 17
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModelRemainder_summable line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModelRemainder_real line 27
  4. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModelRemainder_coefficient line 40
  5. def OAI.CubicFirstMoment.cubicThetaArithmeticModel line 56
  6. def OAI.CubicFirstMoment.cubicThetaArithmeticModelTorus line 60
  7. lemma OAI.CubicFirstMoment.cubicThetaArithmeticModelTorus_real line 64
  8. theorem OAI.CubicFirstMoment.cubicThetaArithmeticModelTorus_coefficient line 71