OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeResidueTestWeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A high radial test adapted to the cubic dilation.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueTestWeight line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueTestWeight_low line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueTestWeight_scale line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueTestWeight_radial_ne_zero line 32