OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimaryPeriodicity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The base theta series has the smaller period lattice 3 Z[omega]. This follows from its actual ramified support, and supplies the upper unipotent stabilizer for the principal level-three group.

  1. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_lambda_dvd line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaFrequency_three_phase line 31
  3. lemma OAI.CubicFirstMoment.cubicThetaArithmeticTerm_three_periodic line 51
  4. theorem OAI.CubicFirstMoment.cubicThetaFunction_three_periodic line 67