OAI/Analysis/IrrationalRotation/Operators/ProjectionAtomOrbit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProjectionAtomOrbit.mul_eq_zero_of_atoms line 16
  2. theorem OAI.Invariant233.ProjectionAtomOrbit.sum_atoms_isStarProjection line 36
  3. theorem OAI.Invariant233.ProjectionAtomOrbit.vectorTrace_le_norm_sq line 53
  4. theorem OAI.Invariant233.ProjectionAtomOrbit.sum_vectorTrace_atoms_le line 62
  5. theorem OAI.Invariant233.ProjectionAtomOrbit.finite_atoms_vectorTrace_ge line 69
  6. theorem OAI.Invariant233.ProjectionAtomOrbit.atom_map line 87
  7. theorem OAI.Invariant233.ProjectionAtomOrbit.atom_iterate line 109
  8. theorem OAI.Invariant233.ProjectionAtomOrbit.finite_atom_orbit line 119
  9. theorem OAI.Invariant233.ProjectionAtomOrbit.exists_positive_atom_period line 138
  10. theorem OAI.Invariant233.ProjectionAtomOrbit.vectorTrace_pos_of_faithful line 157
  11. theorem OAI.Invariant233.ProjectionAtomOrbit.isDiffuse_of_total_ergodicity line 171
  12. theorem OAI.Invariant233.ProjectionAtomOrbit.faithfulTracialVector_restrict line 192
  13. theorem OAI.Invariant233.ProjectionAtomOrbit.vectorTrace_unitary_conjugation line 198