OAI/Analysis/IrrationalRotation/Couplings/CircleCouplingLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CircleCoupling.tag_bounds line 14
2. lemma OAI.Invariant233.CircleCoupling.initialLaw_isProbabilityMeasure line 18
3. lemma OAI.Invariant233.CircleCoupling.coordinateLaw_isProbabilityMeasure line 26
4. lemma OAI.Invariant233.CircleCoupling.law_isProbabilityMeasure line 40
5. lemma OAI.Invariant233.CircleCoupling.measurable_observedDigit line 46
6. lemma OAI.Invariant233.CircleCoupling.measurable_digits line 56
7. lemma OAI.Invariant233.CircleCoupling.measurable_label line 62
8. lemma OAI.Invariant233.CircleCoupling.iCondIndepFun_labels_digits line 65
9. lemma OAI.Invariant233.CircleCoupling.posterior_isMarkov line 76