OAI/NumberTheory/CubicMoment/Theta/CubicThetaCubeCancellation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact primary-cube scaling of the actual dual coefficient and its local Ramanujan factor. These are the algebraic inputs to free-cube removal.

  1. def OAI.CubicFirstMoment.cubicThetaDualCube line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaFrequency_mul_cube line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaLocalCoefficient_cube line 23
  4. def OAI.CubicFirstMoment.cubicThetaCommonTau line 42
  5. lemma OAI.CubicFirstMoment.cubicThetaCommonTau_cube line 45