OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedCuspPeriodicity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Periodicity of the actual translated-cusp row phase. Conjugating a translation by the cusp matrix gives a principal level-nine matrix with trivial Kubota value, proved from the supplementary laws.

  1. def OAI.CubicFirstMoment.cubicThetaCuspTranslationMatrix line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaCuspTranslationMatrix_mem line 17
  3. def OAI.CubicFirstMoment.cubicThetaCuspTranslation line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaCuspTranslation_value line 27
  5. def OAI.CubicFirstMoment.cubicThetaShiftedRowTranslate line 38
  6. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowTranslate_action line 49
  7. def OAI.CubicFirstMoment.cubicThetaShiftedRowPhase line 60
  8. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowPhase_eq line 63
  9. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowPhase_periodic line 69
  10. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowPhase_norm line 77