OAI/NumberTheory/CubicMoment/Theta/CubicThetaFullGaussian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual affine four-dimensional Gaussian, before removal of common primary factors. Its Mellin integral is the full height series.

  1. def OAI.CubicFirstMoment.CubicThetaFullRow.quadratic line 12
  2. lemma OAI.CubicFirstMoment.CubicThetaFullRow.denominator_pos line 15
  3. lemma OAI.CubicFirstMoment.CubicThetaFullRow.quadratic_pos line 25
  4. lemma OAI.CubicFirstMoment.CubicThetaFullRow.height_eq_inv line 28
  5. def OAI.CubicFirstMoment.cubicThetaFullGaussian line 32
  6. lemma OAI.CubicFirstMoment.cubicThetaFullGaussian_summable line 35
  7. lemma OAI.CubicFirstMoment.cubicThetaFullRowCoordinates_quadratic line 50
  8. lemma OAI.CubicFirstMoment.cubicThetaFullGaussian_reindex line 62