OAI/Analysis/IrrationalRotation/Model/BlockedProductCoupling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Invariant233.BlockedProductCoupling.Coordinate line 12
  2. abbrev OAI.Invariant233.BlockedProductCoupling.Sample line 14
  3. def OAI.Invariant233.BlockedProductCoupling.flatten line 16
  4. def OAI.Invariant233.BlockedProductCoupling.leftEndpoint line 19
  5. def OAI.Invariant233.BlockedProductCoupling.rightEndpoint line 23
  6. def OAI.Invariant233.BlockedProductCoupling.toCircle line 27
  7. def OAI.Invariant233.BlockedProductCoupling.circleLeftEndpoint line 30
  8. def OAI.Invariant233.BlockedProductCoupling.circleRightEndpoint line 33
  9. def OAI.Invariant233.BlockedProductCoupling.parameters line 36
  10. def OAI.Invariant233.BlockedProductCoupling.blockLaw line 57
  11. def OAI.Invariant233.BlockedProductCoupling.law line 63
  12. def OAI.Invariant233.BlockedProductCoupling.currentEvent line 67
  13. def OAI.Invariant233.BlockedProductCoupling.futureBad line 72
  14. def OAI.Invariant233.BlockedProductCoupling.retainedEvent line 79