OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootCoverDomain.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.CubicFirstMoment.cubicThetaPrimeRootCoverGroup line 13
  2. instance OAI.CubicFirstMoment.cubicThetaPrimeRootCoverGroup_finiteIndex line 16
  3. instance OAI.CubicFirstMoment.cubicThetaPrimeRootCoverGroup_continuous line 20
  4. abbrev OAI.CubicFirstMoment.CubicThetaPrimeRootCover line 24
  5. def OAI.CubicFirstMoment.cubicThetaPrimeRootCoverMap line 27
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootCoverMap_open line 31
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootCover_covering line 35
  8. def OAI.CubicFirstMoment.cubicThetaPrimeRootTransversal line 39
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootTransversal_complement line 43
  10. instance OAI.CubicFirstMoment.cubicThetaPrimeRootTransversal_finite line 47
  11. def OAI.CubicFirstMoment.cubicThetaPrimeRootCoverDomain line 53
  12. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootCoverDomain_measurable line 57
  13. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootCoverDomain_unique line 64
  14. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootCoverDomain_isFundamentalDomain line 96
  15. instance OAI.CubicFirstMoment.cubicThetaPrimeRootCover_measurableSpace line 102
  16. instance OAI.CubicFirstMoment.cubicThetaPrimeRootCover_borelSpace line 105
  17. def OAI.CubicFirstMoment.cubicThetaPrimeRootCoverMeasure line 108