OAI/NumberTheory/CubicMoment/Theta/CubicThetaSiegelReduction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A Siegel-set reduction for the full Eisenstein modular group, and its finite translate cover of the actual principal level-three quotient.

  1. lemma OAI.CubicFirstMoment.cubicTheta_nearest_normSq_bound line 12
  2. def OAI.CubicFirstMoment.cubicThetaFullTranslation line 28
  3. def OAI.CubicFirstMoment.cubicThetaFullInversion line 31
  4. lemma OAI.CubicFirstMoment.cubicThetaFullTranslation_complex line 34
  5. lemma OAI.CubicFirstMoment.cubicThetaFullInversion_complex line 40
  6. lemma OAI.CubicFirstMoment.cubicThetaFullInversion_height line 47
  7. def OAI.CubicFirstMoment.cubicThetaSiegelSet line 54

    Source documentation

    A single full-group cusp chart with a uniform positive lower height.

    def cubicThetaSiegelSet : Set (ℂ × ℝ) :=
…
  8. theorem OAI.CubicFirstMoment.cubicThetaSiegelSet_meets_orbit line 57
  9. theorem OAI.CubicFirstMoment.cubicThetaFiniteSiegelCover line 87