OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeResidueTestWeight.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A concrete high-cusp test with a nonzero common radial factor for the three unramified residue coordinates.

  1. lemma OAI.CubicFirstMoment.cubicThetaRadialTestWeight_low line 12
  2. def OAI.CubicFirstMoment.cubicThetaPrimeResidueTestWeight line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeResidueTestWeight_low line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeResidueTestWeight_scale line 30
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeResidueTestWeight_radial_ne_zero line 39