OAI/Analysis/Nuclearity/CompletedConjugation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Conjugation on the completed tensor product. Cyclic approximation of finitely many coefficient vectors produces a genuine inner compression, with its implementer in the nonunital algebra.

  1. lemma OAI.WeakPureInfiniteness.tensorCoefficientFunctional_conjugation line 26
  2. lemma OAI.WeakPureInfiniteness.representedCompression_eq line 50
  3. lemma OAI.WeakPureInfiniteness.representedTensorFunctional_inner line 59
  4. lemma OAI.WeakPureInfiniteness.tensorCoefficientFunctional_inner_unitized line 70
  5. theorem OAI.WeakPureInfiniteness.completed_conjugation_inner_approximation line 98
  6. lemma OAI.WeakPureInfiniteness.starHomContinuous_completelyPositive line 129
  7. lemma OAI.WeakPureInfiniteness.representedTensorFunctional_hom line 135