OAI/Analysis/IrrationalRotation/Sampling/ProductPrefixCircle.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.OrderedProductCoupling.circleHybridEndpoint_selected line 13
2. theorem OAI.Invariant233.OrderedProductCoupling.map_prefixPairLaw_circle line 21
3. theorem OAI.Invariant233.OrderedProductCoupling.circle_prefix_first_marginal line 33
4. theorem OAI.Invariant233.OrderedProductCoupling.circle_prefix_second_marginal line 38
5. theorem OAI.Invariant233.OrderedProductCoupling.circle_prefix_absolutelyContinuous_reference line 48
6. theorem OAI.Invariant233.OrderedProductCoupling.map_sum_realTriangularLaw line 55
7. theorem OAI.Invariant233.OrderedProductCoupling.map_absolutelyContinuous_sum_triangularLaw line 61