OAI/NumberTheory/CubicMoment/Theta/CubicThetaEisensteinResidues.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite residue weight used to unfold the cubic Eisenstein series. Its modulus is exactly 3c, with zero extension outside primary coprime rows.

  1. def OAI.CubicFirstMoment.CubicThetaBottomRow.shift line 11
  2. lemma OAI.CubicFirstMoment.CubicThetaBottomRow.shift_c line 14
  3. lemma OAI.CubicFirstMoment.CubicThetaBottomRow.shift_d line 20
  4. lemma OAI.CubicFirstMoment.CubicThetaBottomRow.shift_phase line 26
  5. def OAI.CubicFirstMoment.cubicThetaEisensteinWeight line 30
  6. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_periodic line 33
  7. def OAI.CubicFirstMoment.cubicThetaEisensteinResidueWeight line 54
  8. lemma OAI.CubicFirstMoment.cubicThetaEisensteinResidueWeight_mk line 57