OAI/Analysis/Nuclearity/UnitizedCPMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The unital extension of a completely positive contraction on a nonunital C*-algebra. Matrix Schwarz supplies the positive square defect.

  1. def OAI.WeakPureInfiniteness.unitizedCPLinear line 15
  2. theorem OAI.WeakPureInfiniteness.unitizedCPLinear_inr line 22
  3. theorem OAI.WeakPureInfiniteness.unitizedCPLinear_one line 25
  4. lemma OAI.WeakPureInfiniteness.unitizedCPLinear_product_defect line 30
  5. lemma OAI.WeakPureInfiniteness.unitizedCPLinear_matrix_defect line 54
  6. lemma OAI.WeakPureInfiniteness.matrix_cpc_schwarz line 68
  7. theorem OAI.WeakPureInfiniteness.unitizedCPLinear_cp line 78

    Source documentation

    A cpc map has the canonical unital completely positive extension.

    theorem unitizedCPLinear_cp (φ : A →L[ℂ] B) (hφ : CompletelyPositive φ) (hn : ‖φ‖ ≤ 1) :
    CompletelyPositive (unitizedCPLinear φ) := by
…

    Mentions: OAI.WeakPureInfiniteness.CompletelyPositive, OAI.WeakPureInfiniteness.unitizedCPLinear