OAI/Analysis/KadisonSimilarity/Derivation/NormalCyclicGraph.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A faithful normal finite trace makes the cyclic orbit map closable. The proof removes a high spectral projection of vanishing trace, leaving an arbitrarily small operator applied to the fixed cyclic vector.

  1. theorem OAI.KadisonSimilarity.normal_tracial_cyclic_graph_closable line 26