OAI/Analysis/IrrationalRotation/Model/OneCoordinateCoupling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.OneCoordinateCoupling.baseLaw line 13
  2. def OAI.Invariant233.OneCoordinateCoupling.leftLaw line 15
  3. def OAI.Invariant233.OneCoordinateCoupling.rightLaw line 19
  4. def OAI.Invariant233.OneCoordinateCoupling.pairLaw line 23
  5. instance OAI.Invariant233.OneCoordinateCoupling.labelMeasurableSpace line 28
  6. instance OAI.Invariant233.OneCoordinateCoupling.labelMeasurableSingletonClass line 30
  7. def OAI.Invariant233.OneCoordinateCoupling.labelledLaw line 33
  8. def OAI.Invariant233.OneCoordinateCoupling.intervalDensity line 39
  9. def OAI.Invariant233.OneCoordinateCoupling.leftDensity line 42
  10. def OAI.Invariant233.OneCoordinateCoupling.rightDensity line 46
  11. def OAI.Invariant233.OneCoordinateCoupling.leftMarginalDensity line 51
  12. def OAI.Invariant233.OneCoordinateCoupling.rightMarginalDensity line 55