OAI/Analysis/IrrationalRotation/Rotation/RotationTowerAlgebras.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.Rotation.towerLevel line 14
2. theorem OAI.Invariant233.Rotation.measurableSet_towerLevel line 17
3. theorem OAI.Invariant233.Rotation.powerProjection_mul_eq_zero_of_disjoint line 22
4. def OAI.Invariant233.Rotation.towerMatrixEntries line 32
5. theorem OAI.Invariant233.Rotation.towerMatrixEntries_isBlockMatrixUnitFamily line 37
6. def OAI.Invariant233.Rotation.finiteTowerAlgebra line 58
7. theorem OAI.Invariant233.Rotation.towerMatrixEntries_range line 64
8. theorem OAI.Invariant233.Rotation.finiteTowerAlgebra_eq_blockMatrixAlgebra line 76
9. theorem OAI.Invariant233.Rotation.finiteTowerAlgebra_finiteDimensional line 86
10. theorem OAI.Invariant233.Rotation.finiteTowerAlgebra_le line 94
11. theorem OAI.Invariant233.Rotation.towerEntry_mem_finiteTowerAlgebra line 102
12. theorem OAI.Invariant233.Rotation.finiteTowerAlgebra_le_of_refinement line 109
13. theorem OAI.Invariant233.Rotation.setProjection_eq_sum_shifted_of_partition line 123
14. theorem OAI.Invariant233.Rotation.finiteTowerAlgebra_le_of_set_refinement line 147