OAI/NumberTheory/CubicMoment/Theta/CubicThetaGaussianPowerBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A global quadratic decay bound for the nonzero Gaussian lattice tail.

  1. def OAI.CubicFirstMoment.cubicThetaGaussianPowerConstant line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaGaussianPowerConstant_nonneg line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaLatticeGaussianTail_power_bound line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaLatticeGaussianTail_div_bound line 38