OAI/NumberTheory/CubicMoment/Theta/CubicThetaBoundedScaledMellin.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Entire upper Mellin tails at a positive scale, for the two bounded coefficient families in the actual projected transformation.

  1. def OAI.CubicFirstMoment.cubicThetaBoundedScaledAxis line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaBoundedScaledUpper_locallyIntegrable line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaBoundedScaledUpper_isBigO line 35
  4. lemma OAI.CubicFirstMoment.cubicThetaBoundedScaledUpper_small line 53
  5. theorem OAI.CubicFirstMoment.cubicThetaBoundedScaledUpper_mellinConvergent line 62
  6. theorem OAI.CubicFirstMoment.cubicThetaBoundedScaledUpper_entire line 71