OAI/NumberTheory/CubicMoment/Theta/CubicThetaIntegerPeriodicity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The additional integer translation in the full theta group follows from the proved arithmetic support and the elementary trace pairing.

  1. lemma OAI.CubicFirstMoment.cubicThetaFrequency_integer_phase_cube line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaFrequency_integer_phase_primary line 29
  3. lemma OAI.CubicFirstMoment.cubicThetaFrequency_integer_phase_neg line 51
  4. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_integer_phase line 59
  5. lemma OAI.CubicFirstMoment.cubicThetaArithmeticTerm_integer_periodic line 94
  6. theorem OAI.CubicFirstMoment.cubicThetaArithmetic_integer_periodic line 109
  7. theorem OAI.CubicFirstMoment.cubicThetaNormalizedSeries_integer_periodic line 115