OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteCover.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-cover domains in the fixed arithmetic action. This is used to compare the three root levels without postulating equality of integrals on different covers.

  1. structure OAI.CubicFirstMoment.CubicThetaArithmeticCover line 13
  2. instance OAI.CubicFirstMoment.(instance at line 19) line 19
  3. lemma OAI.CubicFirstMoment.CubicThetaArithmeticCover.fundamental line 23
  4. def OAI.CubicFirstMoment.cubicThetaBaseCover line 27
  5. def OAI.CubicFirstMoment.cubicThetaRelativeSubgroup line 40
  6. instance OAI.CubicFirstMoment.cubicThetaRelativeSubgroup_finiteIndex line 42
  7. def OAI.CubicFirstMoment.cubicThetaRelativeSubgroupEquiv line 47
  8. def OAI.CubicFirstMoment.cubicThetaRelativeTransversal line 54
  9. lemma OAI.CubicFirstMoment.cubicThetaRelativeTransversal_complement line 58
  10. instance OAI.CubicFirstMoment.cubicThetaRelativeTransversal_finite line 62
  11. def OAI.CubicFirstMoment.cubicThetaRelativeDomain line 67
  12. lemma OAI.CubicFirstMoment.cubicThetaRelativeDomain_measurable line 70
  13. lemma OAI.CubicFirstMoment.cubicThetaRelativeDomain_unique line 77
  14. def OAI.CubicFirstMoment.cubicThetaRelativeCover line 113