OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramCubePrimePart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The entire prime-divisible part of the actual positive Gram integral. After a common cube dilation it is the original finite denominator sum, with the exact local multiplier and unchanged original cutoff.

  1. def OAI.CubicFirstMoment.cubicThetaGramPrimePart line 14
  2. theorem OAI.CubicFirstMoment.cubicThetaGramPrimePart_cube line 19