OAI/Analysis/IrrationalRotation/Couplings/CircleConditionalAttenuation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CircleWeights.cocycle_ratio_le_exp_of_crossing line 13
2. theorem OAI.Invariant233.CircleWeights.ae_all_int_finite_floor_support_of_map_ac line 29
3. theorem OAI.Invariant233.CircleWeights.ae_all_int_ratio_bounds_of_map_ac line 42
4. theorem OAI.Invariant233.CircleWeights.finite_conditional_attenuation_of_map_ac line 65
5. theorem OAI.Invariant233.CircleWeights.ae_tagged_ratio_le_exp_of_map_ac line 120
6. theorem OAI.Invariant233.CircleParameterLaws.ae_parameter_ratio_bounds_of_map_ac line 148
7. theorem OAI.Invariant233.CircleParameterLaws.ae_parameter_tagged_ratio_le_exp line 169