OAI/Analysis/IrrationalRotation/Rotation/CocycleWindowBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductCocycle.cocycleVersion_le_one_of_nonneg_time line 13
  2. theorem OAI.Invariant233.ProductCocycle.one_le_cocycleVersion_of_nonpos_time line 26
  3. theorem OAI.Invariant233.ProductCocycle.endpoint_floors_eq_zero line 42
  4. theorem OAI.Invariant233.ProductCocycle.cocycle_window_bounds_of_endpoint_margins line 56
  5. theorem OAI.Invariant233.ProductCocycle.signed_cocycle_window_bounds line 108
  6. theorem OAI.Invariant233.ProductCocycle.endpoint_margins_of_scale line 138
  7. theorem OAI.Invariant233.ProductCocycle.reweighted_coefficient_bounds line 148
  8. theorem OAI.Invariant233.CocycleWindowBounds.floor_forward_eq_zero line 176
  9. theorem OAI.Invariant233.CocycleWindowBounds.floor_backward_eq_zero line 185
  10. theorem OAI.Invariant233.CocycleWindowBounds.floor_forward_le line 193
  11. theorem OAI.Invariant233.CocycleWindowBounds.neg_floor_backward_le line 200
  12. theorem OAI.Invariant233.CocycleWindowBounds.tsum_weighted_le_prefix line 207
  13. theorem OAI.Invariant233.CocycleWindowBounds.signed_floor_sums_le line 217
  14. theorem OAI.Invariant233.CocycleWindowBounds.cocycle_bounds line 269
  15. theorem OAI.Invariant233.CocycleWindowBounds.coefficient_bounds line 288