OAI/Analysis/Nuclearity/CPRepresentationDomain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A unital completely positive extension of a representation is bimodular on that representation. This is the Schwarz-equality step used when extending a commuting tensor representation to obtain a commutant-valued projection.

  1. lemma OAI.WeakPureInfiniteness.cp_extension_representation_mul_left line 19
  2. lemma OAI.WeakPureInfiniteness.cp_extension_representation_mul_right line 31
  3. lemma OAI.WeakPureInfiniteness.cp_extension_commutes line 38