OAI/NumberTheory/CubicMoment/Estimates/HuxleyGaussianEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Expansion and Schur bound for the actual Gaussian-weighted dual polynomial.

  1. def OAI.CubicFirstMoment.huxleyDualPolynomial line 12
  2. lemma OAI.CubicFirstMoment.huxley_weighted_phase_summable line 15
  3. lemma OAI.CubicFirstMoment.huxleyGaussianEnergy_expansion line 22
  4. lemma OAI.CubicFirstMoment.huxleyGaussianEnergy_summable line 40
  5. lemma OAI.CubicFirstMoment.huxleyGaussianEnergy_sum line 53
  6. lemma OAI.CubicFirstMoment.huxleyGaussianEnergy_bound line 73