OAI/NumberTheory/CubicMoment/Estimates/HuxleyGaussianPoisson.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One-dimensional Gaussian Poisson identities for the coordinate majorant.

  1. lemma OAI.CubicFirstMoment.summable_integer_quadratic_exp line 11
  2. lemma OAI.CubicFirstMoment.gaussian_coordinate_poisson line 21