OAI/Analysis/IrrationalRotation/Operators/BicommutantCyclic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.Bicommutant.orbitSubmodule line 13
2. theorem OAI.Invariant233.Bicommutant.mem_orbitSubmodule line 23
3. theorem OAI.Invariant233.Bicommutant.orbit_invariant line 26
4. theorem OAI.Invariant233.Bicommutant.closedOrbit_invariant line 32
5. theorem OAI.Invariant233.Bicommutant.projection_mem_centralizer line 37
6. theorem OAI.Invariant233.Bicommutant.apply_mem_orbit_closure line 51
7. theorem OAI.Invariant233.Bicommutant.exists_single_vector_approximation line 66