OAI/NumberTheory/CubicMoment/Theta/CubicThetaCommonCubeScaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing a primary cube scales the actual three-cusp coefficient by its norm. This includes all zero-extension cases.

  1. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_primaryCube line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedLatticeCoefficient_primaryCube line 27
  3. lemma OAI.CubicFirstMoment.cubicThetaActualCuspCoefficient_primaryCube line 55
  4. theorem OAI.CubicFirstMoment.cubicThetaCommonCuspCoefficient_primaryCube line 64