OAI/Analysis/IrrationalRotation/Couplings/ProductConditionalKernels.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.OrderedProductCoupling.coordinate_right_disintegration line 12
2. lemma OAI.Invariant233.OrderedProductCoupling.coordinate_left_disintegration line 27
3. theorem OAI.Invariant233.OrderedProductCoupling.right_condDistrib_eq_product line 42
4. theorem OAI.Invariant233.OrderedProductCoupling.left_condDistrib_eq_product line 56
5. theorem OAI.Invariant233.OrderedProductCoupling.right_coordinates_conditionally_independent line 70
6. theorem OAI.Invariant233.OrderedProductCoupling.left_coordinates_conditionally_independent line 83
7. theorem OAI.Invariant233.OrderedProductCoupling.right_condDistrib_coordinate_law line 96
8. theorem OAI.Invariant233.OrderedProductCoupling.left_condDistrib_coordinate_law line 109
9. theorem OAI.Invariant233.OrderedProductCoupling.ae_leftEndpoint_mem_unit line 122
10. theorem OAI.Invariant233.OrderedProductCoupling.ae_rightEndpoint_mem_unit line 134