OAI/Analysis/IrrationalRotation/Product/ProductCircleConditioning.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.OrderedProductCoupling.left_condExp_eq_circle line 10
2. theorem OAI.Invariant233.OrderedProductCoupling.right_condExp_eq_circle line 19
3. theorem OAI.Invariant233.OrderedProductCoupling.left_iCondIndepSet_iff_circle line 28
4. theorem OAI.Invariant233.OrderedProductCoupling.right_iCondIndepSet_iff_circle line 41
5. theorem OAI.Invariant233.OrderedProductCoupling.right_threshold_event_ae_eq_circle line 54
6. theorem OAI.Invariant233.OrderedProductCoupling.left_threshold_event_ae_eq_circle line 60
7. theorem OAI.Invariant233.OrderedProductCoupling.right_threshold_condExp_eq_circle line 66
8. theorem OAI.Invariant233.OrderedProductCoupling.left_threshold_condExp_eq_circle line 76
9. theorem OAI.Invariant233.OrderedProductCoupling.right_threshold_iCondIndepSet_iff_circle line 86
10. theorem OAI.Invariant233.OrderedProductCoupling.left_threshold_iCondIndepSet_iff_circle line 104