OAI/Analysis/IrrationalRotation/Rotation/CircleCoefficientBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CircleParameterLaws.sum_flattenedCost_prefix line 14
2. theorem OAI.Invariant233.CircleParameterLaws.coefficientBound_eq_prefix line 38
3. theorem OAI.Invariant233.CircleParameterLaws.exists_future_block line 44
4. theorem OAI.Invariant233.CircleParameterLaws.floor_add_eq_zero_of_upper_exclusion line 54
5. theorem OAI.Invariant233.CircleParameterLaws.floor_sub_eq_zero_of_lower_exclusion line 69
6. theorem OAI.Invariant233.CircleParameterLaws.future_floor_add_zero line 85
7. theorem OAI.Invariant233.CircleParameterLaws.future_floor_sub_zero line 96
8. theorem OAI.Invariant233.CircleParameterLaws.weighted_floor_add_eq_prefix line 107
9. theorem OAI.Invariant233.CircleParameterLaws.weighted_floor_sub_eq_prefix line 121
10. theorem OAI.Invariant233.CircleParameterLaws.exp_weighted_floor_add_le_coefficientBound line 135
11. theorem OAI.Invariant233.CircleParameterLaws.exp_neg_weighted_floor_sub_le_coefficientBound line 160