OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompactHeight.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Heights of all representatives above a compact quotient set are uniformly bounded. The arithmetic denominator bound is essential here: a nonparabolic transformation sends height v to at most 1/v.

  1. def OAI.CubicFirstMoment.cubicThetaPointHeight line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaPointHeight_pos line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaPointHeight_continuous line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaPointHeight_full_smul_le line 21
  5. lemma OAI.CubicFirstMoment.cubicThetaPointHeight_local_bound line 38
  6. theorem OAI.CubicFirstMoment.cubicThetaCompact_all_cusp_height_bound line 86
  7. theorem OAI.CubicFirstMoment.cubicThetaCompact_height_bound line 98