Theorems · Inductive type · functional analysis

CompletelyPositiveMap

(A₁ : Type u_1) →
  (A₂ : Type u_2) →
    [inst : NonUnitalCStarAlgebra A₁] →
      [inst_1 : NonUnitalCStarAlgebra A₂] →
        [inst_2 : PartialOrder A₁] →
          [inst_3 : PartialOrder A₂] → [StarOrderedRing A₁] → [StarOrderedRing A₂] → Type (max u_1 u_2)

A linear map φ : A₁ →ₗ[ℂ] A₂ is called completely positive (CP) if CStarMatrix.mapₗ (Fin k) (Fin k) φ (i.e. applying φ to all entries of a k × k matrix) is also positive for every k ∈ ℕ. Note that Fin k here is hardcoded to avoid having to quantify over types and introduce a new universe parameter. See CompletelyPositiveMap.map_cstarMatrix_nonneg for a version of the property that holds for matrices indexed by any finite type.

Defined in

Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Cited by

5 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

NonUnitalCStarAlgebraNonUnitalCStarAlgebraPartialOrderPartialOrderStarOrderedRingStarOrderedRing