OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRadialResidue.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The known constant term of the arithmetic residue transforms by the critical cubed-prime multiplier under every admissible compact radial test.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCube_mellin_multiplier line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCube_zeroRadialTest line 35
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeCube_residue_radial_observation line 65