OAI/Analysis/IrrationalRotation/Couplings/CircleDigitCoupling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CircleDigitCoupling.baseLaw_bin line 13
2. lemma OAI.Invariant233.CircleDigitCoupling.labelsGivenDigit_singleton line 22
3. lemma OAI.Invariant233.CircleDigitCoupling.endpointLaw_isProbabilityMeasure line 37
4. lemma OAI.Invariant233.CircleDigitCoupling.labelMass_sum line 50
5. lemma OAI.Invariant233.CircleDigitCoupling.rawLaw_isProbabilityMeasure line 69
6. lemma OAI.Invariant233.CircleDigitCoupling.digitWeight_total_ne_zero line 82
7. lemma OAI.Invariant233.CircleDigitCoupling.digitWeight_total_ne_top line 96
8. lemma OAI.Invariant233.CircleDigitCoupling.labelsGivenDigit_isMarkov line 107