OAI/Analysis/IrrationalRotation/Couplings/ProductPrefixConditionalLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductCoordinateSplit.map_split_cond_prefix line 14
2. theorem OAI.Invariant233.OrderedProductCoupling.prefix_payload_cond_map line 44
3. theorem OAI.Invariant233.OrderedProductCoupling.prefixPairLaw_cond_factorization line 69
4. theorem OAI.Invariant233.OrderedProductCoupling.prefixPairLaw_cond_absolutelyContinuous line 89
5. theorem OAI.Invariant233.ProductCoordinateSplit.cond_fintype_pi line 103
6. theorem OAI.Invariant233.OrderedProductCoupling.prefix_label_cond_eq_pi line 125
7. theorem OAI.Invariant233.OrderedProductCoupling.prefix_label_pair_factorization line 143