OAI/NumberTheory/CubicMoment/Theta/CubicThetaCommonCuspCoefficient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The dual three-cusp coefficient before local cube cancellation. All dependence on a coprime additive numerator is in its cubic character.

  1. def OAI.CubicFirstMoment.cubicThetaCommonCuspCoefficient line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaProjectedCoefficient_factor line 15
  3. theorem OAI.CubicFirstMoment.cubicThetaNineGaussMatrix_coefficient line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaCommonCuspCoefficient_bound line 51