OAI/NumberTheory/CubicMoment/Theta/CubicThetaProjectedFunctional.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual primary-projector pair has the published archimedean Gamma quotient before finite arithmetic averaging.

  1. lemma OAI.CubicFirstMoment.cubicThetaProjectedDirichlet_complete line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaSelectedDirichlet_complete line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaGamma_dual_halfplane line 30
  4. theorem OAI.CubicFirstMoment.cubicThetaSelectedDirichlet_gamma line 37
  5. theorem OAI.CubicFirstMoment.cubicThetaProjectedDirichlet_gamma line 55