OAI/NumberTheory/CubicMoment/Theta/CubicThetaFullRows.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Primitive rows of the full Eisenstein modular group. Their proper height function gives the full-group reduction needed for a finite cusp cover of the principal level-three quotient.

  1. structure OAI.CubicFirstMoment.CubicThetaPrimitiveRow line 13
  2. def OAI.CubicFirstMoment.cubicThetaFullComplex line 18
  3. def OAI.CubicFirstMoment.cubicThetaPrimitiveRow line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveRow_surjective line 26
  5. def OAI.CubicFirstMoment.CubicThetaPrimitiveRow.denominator line 34
  6. def OAI.CubicFirstMoment.CubicThetaPrimitiveRow.height line 37
  7. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.denominator_pos line 40
  8. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.height_pos line 51
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveRow_height line 54
  10. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.norm_sum_bound line 57
  11. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveRow_height_superlevel_finite line 82
  12. theorem OAI.CubicFirstMoment.cubicThetaFullGroup_exists_max_height line 104