OAI/NumberTheory/CubicMoment/Estimates/MeanValueGaussianEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Gaussian mean square of the actual integer-frequency polynomial.

  1. def OAI.CubicFirstMoment.meanValueGaussianWeight line 12
  2. lemma OAI.CubicFirstMoment.meanValueGaussian_phase_product line 14
  3. lemma OAI.CubicFirstMoment.meanValueGaussian_expansion line 25
  4. lemma OAI.CubicFirstMoment.meanValueGaussian_integrable line 42
  5. lemma OAI.CubicFirstMoment.meanValueGaussian_integral_bound line 63
  6. lemma OAI.CubicFirstMoment.gaussian_schur_bound line 107
  7. theorem OAI.CubicFirstMoment.integerNormPolynomial_gaussian_meanSquare line 153