OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspStep.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The three-step translation character of a shifted cusp. It supplies the ramified finite Fourier factor before the unramified Gauss sum.

  1. def OAI.CubicFirstMoment.cubicThetaCuspStepMatrix line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaCuspStepMatrix_mem line 14
  3. def OAI.CubicFirstMoment.cubicThetaCuspStep line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaCuspStep_add line 24
  5. lemma OAI.CubicFirstMoment.cubicThetaCuspStep_triple line 34
  6. def OAI.CubicFirstMoment.cubicThetaCuspStepValue line 44
  7. lemma OAI.CubicFirstMoment.cubicThetaCuspStepValue_add line 47
  8. lemma OAI.CubicFirstMoment.cubicThetaCuspStepValue_triple line 52
  9. lemma OAI.CubicFirstMoment.cubicThetaCuspStepValue_periodic line 55
  10. def OAI.CubicFirstMoment.cubicThetaShiftedRowStep line 59
  11. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowStep_action line 67
  12. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowPhase_step line 78
  13. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowWeight_step line 86