OAI/NumberTheory/CubicMoment/Theta/CubicThetaEisenstein.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The cubic Eisenstein series on the principal group, before analytic continuation. The bottom-row reindexing proves its actual automorphy; no transformation formula for the theta coefficients is assumed.

  1. def OAI.CubicFirstMoment.cubicThetaPrincipalComplex line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaPrincipalComplex_apply line 17
  3. def OAI.CubicFirstMoment.CubicThetaBottomRow.height line 20
  4. lemma OAI.CubicFirstMoment.cubicThetaBottomRow_height line 23
  5. lemma OAI.CubicFirstMoment.CubicThetaBottomRow.height_pos line 26
  6. lemma OAI.CubicFirstMoment.CubicThetaBottomRow.height_rightMul line 31
  7. def OAI.CubicFirstMoment.cubicThetaEisensteinTerm line 39
  8. def OAI.CubicFirstMoment.cubicThetaEisenstein line 42
  9. lemma OAI.CubicFirstMoment.cubicThetaEisensteinTerm_translate line 45
  10. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_automorphy line 63

    Source documentation

    Automorphy follows by the exact bijection of primitive bottom rows. Absolute convergence in the initial half-plane is proved separately.

    theorem cubicThetaEisenstein_automorphy (g : cubicThetaPrincipalGroup)
    {p : ℂ × ℝ} (hp : 0 < p.2) (s : ℂ) :
    cubicThetaEisenstein (cubicThetaMobius (cubicThetaPrincipalComplex g) p) s =
      cubicThetaKubotaValue g*cubicThetaEisenstein p s := by
…

    Mentions: OAI.CubicFirstMoment.cubicThetaPrincipalGroup, OAI.CubicFirstMoment.cubicThetaEisenstein, OAI.CubicFirstMoment.cubicThetaMobius, OAI.CubicFirstMoment.cubicThetaPrincipalComplex, OAI.CubicFirstMoment.cubicThetaKubotaValue