OAI/Analysis/IrrationalRotation/Model/CircleDigitMarginals.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.CircleCoupling.hybridDigits line 13
  2. def OAI.Invariant233.CircleCoupling.hybridPoint line 18
  3. def OAI.Invariant233.CircleCoupling.rawDensity line 22
  4. def OAI.Invariant233.CircleCoupling.digitDensity line 27
  5. def OAI.Invariant233.CircleCoupling.digitReference line 32
  6. def OAI.Invariant233.CircleCoupling.marginalBound line 37
  7. def OAI.Invariant233.CircleCoupling.DigitMarginalLaws line 39