OAI/Analysis/IrrationalRotation/Sampling/ProductPrefixDomination.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Invariant233.OrderedProductCoupling.sourcePairLaw_isProbabilityMeasure line 16
2. instance OAI.Invariant233.OrderedProductCoupling.leftTailLaw_isProbabilityMeasure line 21
3. instance OAI.Invariant233.OrderedProductCoupling.baseTailLaw_isProbabilityMeasure line 29
4. lemma OAI.Invariant233.OrderedProductCoupling.assemblePrefixPair_measurable line 34
5. lemma OAI.Invariant233.OrderedProductCoupling.prefixPairsLaw_absolutelyContinuous line 45
6. lemma OAI.Invariant233.OrderedProductCoupling.prefix_payload_map line 58
7. lemma OAI.Invariant233.OrderedProductCoupling.prefixPairLaw_factorization line 87
8. lemma OAI.Invariant233.OrderedProductCoupling.leftEndpoint_map_infinitePi line 101
9. lemma OAI.Invariant233.OrderedProductCoupling.leftTailLaw_absolutelyContinuous line 106
10. lemma OAI.Invariant233.OrderedProductCoupling.prefixPairLaw_absolutelyContinuous line 132