OAI/NumberTheory/CubicMoment/Theta/CubicThetaLaplaceSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Absolute Laplace interchange for the Eisenstein lattice row.

  1. def OAI.CubicFirstMoment.cubicThetaLaplaceTerm line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaLaplaceTerm_norm line 13
  3. lemma OAI.CubicFirstMoment.cubicThetaLaplaceTerm_integrable line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaLaplaceTerm_mass line 31
  5. lemma OAI.CubicFirstMoment.cubicThetaLaplaceTerm_integral line 45
  6. theorem OAI.CubicFirstMoment.cubicTheta_laplace_tsum line 62