OAI/Analysis/Nuclearity/MatrixFunctionalCP.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A positive functional on a matrix algebra yields a completely positive map into scalar matrices. The construction uses its GNS representation and a finite family of matrix-unit vectors.

  1. def OAI.WeakPureInfiniteness.matrixSingle line 22
  2. lemma OAI.WeakPureInfiniteness.matrixSingle_star line 26
  3. lemma OAI.WeakPureInfiniteness.matrixSingle_mul line 32
  4. lemma OAI.WeakPureInfiniteness.matrixDiagonal_mul_single line 39
  5. def OAI.WeakPureInfiniteness.finiteVectorSynthesis line 51
  6. lemma OAI.WeakPureInfiniteness.finiteVectorSynthesis_basis line 58
  7. def OAI.WeakPureInfiniteness.matrixFunctionalVectors line 63
  8. def OAI.WeakPureInfiniteness.matrixFunctionalRepresentation line 67
  9. def OAI.WeakPureInfiniteness.matrixFunctionalCP line 71
  10. theorem OAI.WeakPureInfiniteness.matrixFunctionalCP_completelyPositive line 78
  11. theorem OAI.WeakPureInfiniteness.matrixFunctionalCP_entry line 84
  12. theorem OAI.WeakPureInfiniteness.matrixFunctionalCP_exists_dilation line 106

    Source documentation

    The reconstructed map has a concrete unital Stinespring representation. Only its value at the unit is needed to bound the compression operator.

    theorem matrixFunctionalCP_exists_dilation (p : Fin n)
    (σ : CStarMatrix (Fin n) (Fin n) A →ₚ[ℂ] ℂ)
    (hn : ‖matrixFunctionalCP p σ 1‖ ≤ 1) :
    ∃ (H : ComplexHilbert.{u}), ∃ (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)),
      ∃ (V : EuclideanSpace ℂ (Fin n) →L[ℂ] H), ‖V‖ ≤ 1 ∧
        ∀ a, scalarMatrixOperatorEquiv (Fin n) (matrixFunctionalCP p σ a) =
          V.adjoint.comp ((π a).comp V) := by
…

    Mentions: OAI.WeakPureInfiniteness.matrixFunctionalCP, OAI.WeakPureInfiniteness.scalarMatrixOperatorEquiv