OAI/NumberTheory/CubicMoment/Theta/CubicThetaResidueCusps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A concrete rational-cusp lift on every residue. Nonunit residues get an arbitrary determinant-one lift, and their cubic character weight is zero.

  1. lemma OAI.CubicFirstMoment.cubicThetaProjectedCoefficient_congr line 13
  2. def OAI.CubicFirstMoment.cubicThetaResidueCuspMatrix line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaResidueCuspMatrix_of_coprime line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaResidueCuspMatrix_bottom line 29
  5. theorem OAI.CubicFirstMoment.cubicThetaResidueCuspPrimary line 36
  6. lemma OAI.CubicFirstMoment.cubicThetaResidueCuspMatrix_cusp line 41
  7. lemma OAI.CubicFirstMoment.cubicThetaResidueCuspMatrix_weighted line 51