OAI/Analysis/IrrationalRotation/Couplings/OneCoordinateConditional.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.OneCoordinateCoupling.finite_total line 13
2. lemma OAI.Invariant233.OneCoordinateCoupling.rightGivenLeft_isMarkov line 28
3. lemma OAI.Invariant233.OneCoordinateCoupling.leftGivenRight_isMarkov line 38
4. lemma OAI.Invariant233.OneCoordinateCoupling.rightGivenLeft_disintegration line 48
5. lemma OAI.Invariant233.OneCoordinateCoupling.leftGivenRight_disintegration line 77