OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticDistribution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The continued family tested against actual compact automorphic sections. On the initial half-plane these are the literal quotient integrals of the arithmetic Eisenstein remainder.

  1. def OAI.CubicFirstMoment.cubicThetaArithmeticDistribution line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaArithmeticDistribution_meromorphic line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaArithmeticDistribution_right line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaArithmeticDistribution_chart_right line 32