OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCoverDomain.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A measurable fundamental domain for the prime cover, obtained from finitely many translates of the original proved fundamental domain.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeTransversal line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeTransversal_complement line 16
  3. instance OAI.CubicFirstMoment.cubicThetaPrimeTransversal_finite line 20
  4. def OAI.CubicFirstMoment.cubicThetaPrimeCoverDomain line 26
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCoverDomain_measurable line 30
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeCoverDomain_unique line 37
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeCoverDomain_isFundamentalDomain line 69
  8. instance OAI.CubicFirstMoment.cubicThetaPrimeCover_measurableSpace line 75
  9. instance OAI.CubicFirstMoment.cubicThetaPrimeCover_borelSpace line 78
  10. def OAI.CubicFirstMoment.cubicThetaPrimeCoverMeasure line 81