OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramCubeResidueBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual cubic-frequency residue is controlled by the exact prime-free Gram correction. No bound for that correction is assumed.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCube_pole_scale line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaFourierResidue_cube_gram_bound line 26