OAI/NumberTheory/CubicMoment/Estimates/GaussianRapidDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial-times-Gaussian bounds at the original computational limits.

  1. lemma OAI.CubicFirstMoment.gaussian_power_bound line 9
  2. lemma OAI.CubicFirstMoment.gaussian_polynomial_bound line 45