OAI/Analysis/IrrationalRotation/Rotation/ProjectionCocycleWindow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.ProjectionCocycleWindow.basisZero line 13
2. theorem OAI.Invariant233.ProjectionCocycleWindow.norm_basisZero line 15
3. theorem OAI.Invariant233.ProjectionCocycleWindow.basisZero_zero line 18
4. theorem OAI.Invariant233.ProjectionCocycleWindow.projection_vector_norm_le line 21
5. theorem OAI.Invariant233.ProjectionCocycleWindow.complement_vector_norm_le line 28
6. theorem OAI.Invariant233.ProjectionCocycleWindow.projection_central_eq_norm_sq line 32
7. theorem OAI.Invariant233.ProjectionCocycleWindow.central_lower_bounds line 39
8. theorem OAI.Invariant233.ProjectionCocycleWindow.product_coefficient_properties line 52
9. theorem OAI.Invariant233.ProjectionCocycleWindow.circle_coefficient_properties line 77