OAI/Analysis/IrrationalRotation/Model/CircleDigitCoupling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Invariant233.CircleDigitCoupling.Label line 13
  2. abbrev OAI.Invariant233.CircleDigitCoupling.CoordinateSample line 14
  3. def OAI.Invariant233.CircleDigitCoupling.endpointLaw line 16
  4. def OAI.Invariant233.CircleDigitCoupling.endpointDensity line 20
  5. def OAI.Invariant233.CircleDigitCoupling.marginalDensity line 24
  6. def OAI.Invariant233.CircleDigitCoupling.labelMass line 28
  7. def OAI.Invariant233.CircleDigitCoupling.rawLaw line 32
  8. def OAI.Invariant233.CircleDigitCoupling.endpoint line 37
  9. def OAI.Invariant233.CircleDigitCoupling.bin line 40
  10. def OAI.Invariant233.CircleDigitCoupling.digitJoint line 43
  11. def OAI.Invariant233.CircleDigitCoupling.digitWeight line 48
  12. def OAI.Invariant233.CircleDigitCoupling.labelsGivenDigit line 52
  13. def OAI.Invariant233.CircleDigitCoupling.width line 58
  14. def OAI.Invariant233.CircleDigitCoupling.topLabel line 60
  15. def OAI.Invariant233.CircleDigitCoupling.bottomLabel line 61