OAI/Analysis/IrrationalRotation/Sampling/PrefixCocycleCap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.finite_floor_support_selectedEndpoint line 11
2. theorem OAI.Invariant233.ProductModel.ae_pair_all_int_finite_floor_support line 27
3. theorem OAI.Invariant233.ProductModel.ae_ordered_cocycle_ratio_cap line 46
4. theorem OAI.Invariant233.ProductModel.ae_all_selected_cocycle_ratio_cap line 65
5. theorem OAI.Invariant233.ProductModel.measurableSet_all_cocycle_ratio_cap line 86
6. theorem OAI.Invariant233.ProductModel.prefixPairLaw_cocycle_ratio_cap line 100