OAI/Analysis/IrrationalRotation/Model/CircleCoupling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Invariant233.CircleCoupling.Sample line 13
  2. def OAI.Invariant233.CircleCoupling.initialLaw line 15
  3. def OAI.Invariant233.CircleCoupling.tag line 18
  4. def OAI.Invariant233.CircleCoupling.coordinateLaw line 20
  5. def OAI.Invariant233.CircleCoupling.law line 25
  6. def OAI.Invariant233.CircleCoupling.observedDigit line 28
  7. def OAI.Invariant233.CircleCoupling.digits line 33
  8. def OAI.Invariant233.CircleCoupling.point line 37
  9. def OAI.Invariant233.CircleCoupling.label line 40
  10. def OAI.Invariant233.CircleCoupling.posterior line 42