OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootHeckeIntegral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-index integral transport to the actual cubic root domain. The statement is used for real masses and complex pairings alike.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHecke_disjoint line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHecke_relative_integrable line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHecke_integrable line 40
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHecke_integral line 51