Completely Positive maps

Building on MatrixMaps, this defines the Props: IsHermitianPreserving, IsPositive and IsCompletelyPositive. They have basic facts such as closure under composition, addition, and scaling.

def MatrixMap.IsHermitianPreserving {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] (M : MatrixMap A B R) : Prop

A linear matrix map is Hermitian preserving if it maps IsHermitian matrices to IsHermitian.

Equations

• M.IsHermitianPreserving = ∀ {x : Matrix A A R}, x.IsHermitian → (M x).IsHermitian

def MatrixMap.IsPositive {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] (M : MatrixMap A B R) : Prop

A linear matrix map is positive if it maps PosSemidef matrices to PosSemidef.

Equations

• M.IsPositive = ∀ {x : Matrix A A R}, x.PosSemidef → (M x).PosSemidef

def MatrixMap.IsCompletelyPositive {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] (M : MatrixMap A B R) : Prop

A linear matrix map is completely positive if, for any integer n, the tensor product with I(n) is positive.

Equations

• M.IsCompletelyPositive = ∀ (n : ℕ), (M.kron LinearMap.id).IsPositive

theorem MatrixMap.IsHermitianPreserving.id {R : Type u_4} [RCLike R] {A : Type u_5} [Fintype A] : (MatrixMap.id A R).IsPositive

The identity MatrixMap IsHermitianPreserving.

theorem MatrixMap.IsHermitianPreserving.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {R : Type u_4} [RCLike R] {M₁ : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M₁.IsHermitianPreserving) (h₂ : M₂.IsHermitianPreserving) : IsHermitianPreserving (M₂ ∘ₗ M₁)

The composition of IsHermitianPreserving maps is also Hermitian preserving.

theorem MatrixMap.IsPositive.IsHermitianPreserving {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] (M : MatrixMap A B R) (hM : M.IsPositive) : M.IsHermitianPreserving

theorem MatrixMap.IsPositive.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [Fintype C] {M₁ : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M₁.IsPositive) (h₂ : M₂.IsPositive) : IsPositive (M₂ ∘ₗ M₁)

The composition of IsPositive maps is also positive.

theorem MatrixMap.IsPositive.id {R : Type u_4} [RCLike R] {A : Type u_5} [Fintype A] : (MatrixMap.id A R).IsPositive

The identity MatrixMap IsPositive.

theorem MatrixMap.IsPositive.add {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] {M₁ M₂ : MatrixMap A B R} (h₁ : M₁.IsPositive) (h₂ : M₂.IsPositive) : (M₁ + M₂).IsPositive

Sums of IsPositive maps are IsPositive.

theorem MatrixMap.IsPositive.smul {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] {M : MatrixMap A B R} (hM : M.IsPositive) {x : R} (hx : 0 ≤ x) : (x • M).IsPositive

Nonnegative scalings of IsPositive maps are IsPositive.

theorem MatrixMap.IsCompletelyPositive.of_Fintype {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {M : MatrixMap A B R} (h : M.IsCompletelyPositive) (T : Type u_5) [Fintype T] [DecidableEq T] : (M.kron LinearMap.id).IsPositive

Definition of a CP map, but with Fintype T in the definition instead of a Fin n.

theorem MatrixMap.IsCompletelyPositive.IsPositive {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq A] {M : MatrixMap A B R} (hM : M.IsCompletelyPositive) : M.IsPositive

theorem MatrixMap.IsCompletelyPositive.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] [DecidableEq B] {M₁ : MatrixMap A B R} {M₂ : MatrixMap B C R} (h₁ : M₁.IsCompletelyPositive) (h₂ : M₂.IsCompletelyPositive) : IsCompletelyPositive (M₂ ∘ₗ M₁)

The composition of IsCompletelyPositive maps is also completely positive.

theorem MatrixMap.IsCompletelyPositive.id {A : Type u_1} {R : Type u_4} [RCLike R] [Fintype A] [DecidableEq A] : (MatrixMap.id A R).IsCompletelyPositive

The identity MatrixMap IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.add {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {M₁ M₂ : MatrixMap A B R} (h₁ : M₁.IsCompletelyPositive) (h₂ : M₂.IsCompletelyPositive) : (M₁ + M₂).IsCompletelyPositive

Sums of IsCompletelyPositive maps are IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.smul {A : Type u_1} {B : Type u_2} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] {M : MatrixMap A B R} (hM : M.IsCompletelyPositive) {x : R} (hx : 0 ≤ x) : (x • M).IsCompletelyPositive

Nonnegative scalings of IsCompletelyPositive maps are IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.zero (A : Type u_1) (B : Type u_2) {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [DecidableEq A] : IsCompletelyPositive 0

The zero map IsCompletelyPositive.

theorem MatrixMap.IsCompletelyPositive.kron_kronecker_const {d : Type u_5} {A : Type u_1} {R : Type u_4} [RCLike R] [Fintype A] [DecidableEq A] [Fintype d] [DecidableEq d] {C : Matrix d d R} (h : C.PosSemidef) {h₁ : ∀ (x y : Matrix A A R), (fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C) (x + y) = (fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C) x + (fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C) y} {h₂ : ∀ (m : R) (x : Matrix A A R), { toFun := fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C, map_add' := h₁ }.toFun x} : IsCompletelyPositive { toFun := fun (M : Matrix A A R) => Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) M C, map_add' := h₁, map_smul' := h₂ }

The map that takes M and returns M ⊗ₖ C, where C is positive semidefinite, is a completely positive map.

theorem MatrixMap.choi_PSD_iff_CP_map {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq A] (M : MatrixMap A B ℂ) : M.IsCompletelyPositive ↔ M.choi_matrix.PosSemidef

Choi's theorem on completely positive maps: A map IsCompletelyPositive iff its Choi Matrix is PSD.

theorem MatrixMap.IsCompletelyPositive.kron {A : Type u_1} {B : Type u_2} {C : Type u_3} {R : Type u_4} [RCLike R] [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] {D : Type u_5} [DecidableEq C] [Fintype D] {M₁ : MatrixMap A B R} {M₂ : MatrixMap C D R} (h₁ : M₁.IsCompletelyPositive) (h₂ : M₂.IsCompletelyPositive) : (M₁.kron M₂).IsCompletelyPositive

The Kronecker product of IsCompletelyPositive maps is also completely positive.

theorem MatrixMap.IsCompletelyPositive.piKron {R : Type u_4} [RCLike R] {ι : Type u} [DecidableEq ι] [fι : Fintype ι] {dI : ι → Type v} [(i : ι) → Fintype (dI i)] [(i : ι) → DecidableEq (dI i)] {dO : ι → Type w} [(i : ι) → Fintype (dO i)] [(i : ι) → DecidableEq (dO i)] {Λi : (i : ι) → MatrixMap (dI i) (dO i) R} (h₁ : ∀ (i : ι), (Λi i).IsCompletelyPositive) : (MatrixMap.piKron Λi).IsCompletelyPositive

The piKron product of IsCompletelyPositive maps is also completely positive.