OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootCoverDomain.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverGroup line 13
  2. instance OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverGroup_finiteIndex line 16
  3. instance OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverGroup_continuous line 20
  4. abbrev OAI.CubicFirstMoment.CubicThetaPrimeCubeRootCover line 24
  5. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverMap line 27
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverMap_open line 31
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCover_covering line 35
  8. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootTransversal line 39
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootTransversal_complement line 43
  10. instance OAI.CubicFirstMoment.cubicThetaPrimeCubeRootTransversal_finite line 47
  11. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverDomain line 53
  12. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverDomain_measurable line 57
  13. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverDomain_unique line 64
  14. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverDomain_isFundamentalDomain line 96
  15. instance OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCover_measurableSpace line 102
  16. instance OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCover_borelSpace line 105
  17. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootCoverMeasure line 108