OAI/Analysis/Commutator/OrbitFixedTrace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.OrbitStateHull.act_vector line 22
2. lemma OAI.Kadison.OrbitStateHull.orbit_invariant line 30
3. lemma OAI.Kadison.OrbitStateHull.hull_invariant line 40
4. theorem OAI.Kadison.OrbitStateHull.exists_tracial_hull_of_norm_separable line 60