OAI/Analysis/IrrationalRotation/Couplings/ProductCoupling.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Invariant233.OrderedProductCoupling.coordinateLaw_isProbabilityMeasure line 14
2. instance OAI.Invariant233.OrderedProductCoupling.law_isProbabilityMeasure line 19
3. instance OAI.Invariant233.OrderedProductCoupling.baseMeasure_isProbabilityMeasure line 23
4. lemma OAI.Invariant233.OrderedProductCoupling.leftEndpoint_measurable line 27
5. lemma OAI.Invariant233.OrderedProductCoupling.rightEndpoint_measurable line 31
6. lemma OAI.Invariant233.OrderedProductCoupling.hybridEndpoint_measurable line 35
7. lemma OAI.Invariant233.OrderedProductCoupling.coordinateLaw_map_pair line 41
8. lemma OAI.Invariant233.OrderedProductCoupling.coordinateLaw_map_left line 45
9. lemma OAI.Invariant233.OrderedProductCoupling.coordinateLaw_map_right line 54
10. lemma OAI.Invariant233.OrderedProductCoupling.hybridEndpoint_map line 63
11. lemma OAI.Invariant233.OrderedProductCoupling.ae_ordered line 82
12. lemma OAI.Invariant233.OrderedProductCoupling.coordinates_independent line 90
13. lemma OAI.Invariant233.OrderedProductCoupling.marginalDensity_memLp line 94
14. lemma OAI.Invariant233.OrderedProductCoupling.marginalDensity_nonneg line 100
15. lemma OAI.Invariant233.OrderedProductCoupling.marginalDensity_integral line 110
16. lemma OAI.Invariant233.OrderedProductCoupling.marginalDensity_variance_le line 119
17. lemma OAI.Invariant233.OrderedProductCoupling.exists_hybrid_density line 130