OAI/Analysis/IrrationalRotation/Couplings/BlockedProductCoupling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.BlockedProductCoupling.coordinate_isProbabilityMeasure line 21
2. theorem OAI.Invariant233.BlockedProductCoupling.blockLaw_isProbabilityMeasure line 28
3. theorem OAI.Invariant233.BlockedProductCoupling.law_isProbabilityMeasure line 34
4. theorem OAI.Invariant233.BlockedProductCoupling.law_map_block line 40
5. theorem OAI.Invariant233.BlockedProductCoupling.law_map_coordinate line 45
6. theorem OAI.Invariant233.BlockedProductCoupling.currentEvent_mass line 54
7. theorem OAI.Invariant233.BlockedProductCoupling.law_map_uncurry line 85
8. theorem OAI.Invariant233.BlockedProductCoupling.law_left_marginal_le_ten line 99
9. theorem OAI.Invariant233.BlockedProductCoupling.law_right_marginal_le_ten line 114
10. theorem OAI.Invariant233.BlockedProductCoupling.futureBad_mass_le line 129