OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramCubeCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reindex the cube-divisible denominators with the two scaled positive cutoffs. The finite norm cutoff is retained exactly.

  1. lemma OAI.CubicFirstMoment.cubicThetaGramDenominators_cube_scale line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaGramDenominators_cube_sum line 33