OAI/NumberTheory/CubicMoment/Theta/CubicThetaBorelSection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A measurable choice of representatives for the actual principal quotient, obtained from a countable disjoint refinement of covering charts.

  1. instance OAI.CubicFirstMoment.cubicThetaPoint_measurableSpace line 14
  2. instance OAI.CubicFirstMoment.cubicThetaPoint_borelSpace line 15
  3. instance OAI.CubicFirstMoment.cubicThetaQuotient_measurableSpace line 16
  4. instance OAI.CubicFirstMoment.cubicThetaQuotient_borelSpace line 17
  5. lemma OAI.CubicFirstMoment.cubicThetaQuotientChart_source_eq line 19
  6. lemma OAI.CubicFirstMoment.cubicTheta_countable_chart_cover line 28
  7. def OAI.CubicFirstMoment.cubicThetaAtlasCenter line 46
  8. def OAI.CubicFirstMoment.cubicThetaAtlasOpen line 49
  9. def OAI.CubicFirstMoment.cubicThetaAtlasPiece line 52
  10. lemma OAI.CubicFirstMoment.cubicThetaAtlasPiece_measurable line 55
  11. lemma OAI.CubicFirstMoment.cubicThetaAtlasPiece_cover line 58
  12. def OAI.CubicFirstMoment.cubicThetaAtlasLocalLift line 65
  13. lemma OAI.CubicFirstMoment.cubicThetaAtlasLocalLift_measurable line 70
  14. lemma OAI.CubicFirstMoment.cubicThetaAtlasLocalLift_rightInverse line 78
  15. lemma OAI.CubicFirstMoment.cubicTheta_measurable_section_exists line 87