OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompactCoreCover.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A finite compact-core and cusp cover of the principal quotient. All charts are actual hyperbolic transformations of the single Siegel set.

  1. def OAI.CubicFirstMoment.cubicThetaSiegelCore line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaSiegelCore_compact line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaSiegelCore_positive line 19
  4. def OAI.CubicFirstMoment.cubicThetaCompactCore line 24
  5. def OAI.CubicFirstMoment.cubicThetaCuspCharts line 27
  6. lemma OAI.CubicFirstMoment.cubicThetaCompactCore_compact line 30
  7. lemma OAI.CubicFirstMoment.cubicThetaSiegelSet_mem_core line 37
  8. theorem OAI.CubicFirstMoment.cubicThetaCompactCoreCuspCover line 45