OAI/NumberTheory/CubicMoment/Estimates/HuxleyGaussianCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence and the two-coordinate theta identity.

  1. def OAI.CubicFirstMoment.huxleyCoordinateEquiv line 10
  2. def OAI.CubicFirstMoment.huxleyDualCoordinateEquiv line 14
  3. lemma OAI.CubicFirstMoment.summable_real_gaussian_shift line 27
  4. def OAI.CubicFirstMoment.huxleyGaussianFactor line 40
  5. lemma OAI.CubicFirstMoment.norm_huxleyGaussianFactor line 44
  6. lemma OAI.CubicFirstMoment.summable_norm_huxleyGaussianFactor line 50
  7. lemma OAI.CubicFirstMoment.huxley_gaussian_two_coordinate_poisson line 55