OAI/NumberTheory/CubicMoment/Estimates/ThetaMellinSplit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The completed theta Mellin transform as two rapidly convergent tails.

  1. def OAI.CubicFirstMoment.thetaUpper line 11
  2. lemma OAI.CubicFirstMoment.mellin_thetaUpper line 13
  3. lemma OAI.CubicFirstMoment.thetaUpper_mellinConvergent line 20
  4. lemma OAI.CubicFirstMoment.theta_mellin_split line 31