OAI/Analysis/IrrationalRotation/Couplings/CircleCouplingCrossings.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CircleCoupling.coordinate_point_eq_tail line 14
2. lemma OAI.Invariant233.CircleCoupling.coordinate_point_mem_bin line 25
3. lemma OAI.Invariant233.CircleCoupling.ae_top_posterior_lower line 36
4. lemma OAI.Invariant233.CircleCoupling.ae_bottom_posterior_lower line 62