OAI/Analysis/IrrationalRotation/Operators/JointEigenspaceAlgebra.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.JointEigenspaceAlgebra.commute_rankOne_of_same_eigenvalue line 16
2. theorem OAI.Invariant233.JointEigenspaceAlgebra.exists_scalar_on_common_eigenspace line 29
3. theorem OAI.Invariant233.JointEigenspaceAlgebra.commute_starProjection_of_maps line 63
4. theorem OAI.Invariant233.JointEigenspaceAlgebra.common_eigenspace_mapsTo line 81
5. theorem OAI.Invariant233.JointEigenspaceAlgebra.common_eigenspace_projection_mem_bicommutant line 94
6. theorem OAI.Invariant233.JointEigenspaceAlgebra.eq_zero_or_eq_joint_projection_of_le line 110
7. theorem OAI.Invariant233.JointEigenspaceAlgebra.exists_minimal_projection_below_of_joint_eigenspaces line 140
8. theorem OAI.Invariant233.JointEigenspaceAlgebra.atomic_bicommutant_of_dense_joint_eigenspaces line 198