OAI/NumberTheory/CubicMoment/Theta/CubicThetaFullGaussianLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The leading heat coefficient of the actual four-dimensional affine lattice. The limit is independent of the upper-half-space point.

  1. lemma OAI.CubicFirstMoment.cubicThetaLatticeGaussianTail_tendsto_zero line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaLatticeGaussianTail_tendsto_div line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaScalarGaussian_lead_product line 26
  4. theorem OAI.CubicFirstMoment.cubicThetaFullGaussian_leading line 34