OAI/Analysis/OperatorAlgebra/FunctionalCommutant.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The simultaneous representing operators lie in a genuine closed commutant C*-algebra. This is the second tensor factor in KR02 7.18.

  1. def OAI.WeakPureInfiniteness.representationCommutant line 16
  2. instance OAI.WeakPureInfiniteness.representationCommutant_closed line 19
  3. instance OAI.WeakPureInfiniteness.representationCommutant_cstar line 23
  4. lemma OAI.WeakPureInfiniteness.mem_representationCommutant line 27
  5. lemma OAI.WeakPureInfiniteness.representationCommutant_commute line 34
  6. lemma OAI.WeakPureInfiniteness.gns_vector_cyclic line 38
  7. theorem OAI.WeakPureInfiniteness.finite_functionals_in_commutant line 51