OAI/Analysis/IrrationalRotation/Sampling/CircleDigitDisintegration.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CircleDigitCoupling.map_label_observe line 11
2. lemma OAI.Invariant233.CircleDigitCoupling.observed_pair_left line 21
3. lemma OAI.Invariant233.CircleDigitCoupling.observed_pair_right line 29
4. lemma OAI.Invariant233.CircleDigitCoupling.endpointLaw_ae_unit line 42
5. lemma OAI.Invariant233.CircleDigitCoupling.endpointLaw_quantize_singleton line 58
6. lemma OAI.Invariant233.CircleDigitCoupling.digitJoint_eq_sum line 67
7. lemma OAI.Invariant233.CircleDigitCoupling.digitJoint_singleton line 108
8. lemma OAI.Invariant233.CircleDigitCoupling.digitJoint_fst_singleton line 125
9. lemma OAI.Invariant233.CircleDigitCoupling.labelsGivenDigit_disintegration line 141