Positive maps, completely positive maps, density matrices, and quantum channels

This file defines positive maps, completely positive (CP) maps, trace-preserving maps, and quantum channels on M_D(ℂ), together with the basic theory of density matrices (compactness, convexity), following Chapters 3 and 6 of Wolf's lecture notes.

Main results

• IsPositiveMap: a linear map that preserves the PSD cone
• IsTraceNonincreasingMap: a linear endomorphism that does not increase the trace of positive semidefinite inputs
• IsCPMap: a linear map that admits a Kraus representation
• IsKrausCP: a linear map between possibly different matrix algebras that admits a rectangular Kraus representation
• IsCompletelyCopositiveMap: a map whose composition with transposition is CP
• IsDecomposablePositiveMap: a sum of a CP map and a completely copositive map
• IsIndecomposablePositiveMap: a positive map that is not decomposable
• IsCPMap.isPositiveMap: completely positive maps are positive
• IsChannel: completely positive + trace-preserving (CPTP)
• Matrix.transposeLinearMapComplex_isPositiveMap: matrix transposition is positive
• Matrix.transposeLinearMapComplex_isTracePreservingMap: matrix transposition is trace-preserving
• IsPositiveMap.map_isHermitian: positive maps preserve Hermiticity
• densityMatrices_isCompact: the set of density matrices is compact
• densityMatrices_isConvex: the set of density matrices is convex
• IsChannel.map_densityMatrices: channels map density matrices to density matrices

References

• [M. Wolf, Quantum Channels & Operations: Guided Tour, Chapters 3 and 6][Wolf2012QChannels]

Positive maps

def IsPositiveMap {m : Type u_1} {n : Type u_2} (E : Matrix n n ℂ →ₗ[ℂ] Matrix m m ℂ) : Prop

A linear map E : M_n(ℂ) →ₗ[ℂ] M_m(ℂ) is positive if it maps positive semidefinite matrices to positive semidefinite matrices.

Equations

• IsPositiveMap E = ∀ (X : Matrix n n ℂ), X.PosSemidef → (E X).PosSemidef

def IsTracePreservingMap {n : Type u_2} [Fintype n] (E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : Prop

A linear map is trace-preserving if Tr(E(X)) = Tr(X) for all X.

Equations

• IsTracePreservingMap E = ∀ (X : Matrix n n ℂ), (E X).trace = X.trace

def IsTraceNonincreasingMap {n : Type u_2} [Fintype n] (E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : Prop

A matrix endomorphism is trace-nonincreasing if it does not increase the trace of any positive semidefinite input.

Equations

• IsTraceNonincreasingMap E = ∀ (X : Matrix n n ℂ), X.PosSemidef → (E X).trace ≤ X.trace

theorem IsTracePreservingMap.isTraceNonincreasingMap {n : Type u_2} [Fintype n] {E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hE : IsTracePreservingMap E) : IsTraceNonincreasingMap E

Every trace-preserving matrix endomorphism is trace-nonincreasing.

def IsCPMap {n : Type u_2} [Fintype n] (E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : Prop

A linear map is completely positive if it admits a Kraus representation: E(X) = ∑ᵢ Kᵢ X Kᵢ† for some family of operators {Kᵢ}.

Equivalently (by Choi's theorem), E is completely positive iff E ⊗ idₙ is positive for all n. We use the Kraus characterisation since it matches the formulation used in the Kadison–Schwarz and multiplicative-domain proofs.

Equations

• IsCPMap E = ∃ (r : ℕ) (K : Fin r → Matrix n n ℂ), ∀ (X : Matrix n n ℂ), E X = ∑ i : Fin r, K i * X * (K i).conjTranspose

def IsKrausCP {α : Type u_3} {β : Type u_4} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (S : Matrix α α ℂ →ₗ[ℂ] Matrix β β ℂ) : Prop

A completely positive map between possibly different matrix algebras, in rectangular Kraus form: S(X) = ∑ᵢ Aᵢ X Aᵢ†, where Aᵢ : Matrix β α ℂ.

This is the dimension-changing Kraus notion in [M. Wolf, Quantum Channels & Operations: Guided Tour, Section 2.1, Theorem 2.1][Wolf2012QChannels]. It is also the notion used for the support formula of the Petz transpose map in Hayden--Jozsa--Petz--Winter, arXiv:quant-ph/0304007v2, Theorem 3, equation (8). No trace-preservation condition is included.

Equations

• IsKrausCP S = ∃ (r : ℕ) (A : Fin r → Matrix β α ℂ), ∀ (X : Matrix α α ℂ), S X = ∑ i : Fin r, A i * X * (A i).conjTranspose

structure IsChannel {n : Type u_2} [Fintype n] (E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : Prop

A quantum channel is a completely positive trace-preserving (CPTP) map.

This matches the standard definition in quantum information theory (see \cite[Definition 4.1]{Wolf2012Quantum}). Earlier versions of this formalisation required only positivity; the upgrade to complete positivity is important because the Kadison–Schwarz inequality and the multiplicative domain characterisation require CP, not merely positivity.

• cp : IsCPMap E
• tp : IsTracePreservingMap E

def Matrix.transposeLinearMapComplex (n : Type u_1) : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ

Matrix transposition as a complex-linear map on M_n(ℂ).

Equations

• Matrix.transposeLinearMapComplex n = ↑(Matrix.transposeLinearEquiv n n ℂ ℂ)

theorem Matrix.transposeLinearMapComplex_isPositiveMap {n : Type u_2} : IsPositiveMap (transposeLinearMapComplex n)

Matrix transposition preserves positive semidefinite matrices.

theorem Matrix.transposeLinearMapComplex_isTracePreservingMap {n : Type u_2} [Fintype n] : IsTracePreservingMap (transposeLinearMapComplex n)

Matrix transposition preserves the trace.

def IsCompletelyCopositiveMap {n : Type u_1} [Fintype n] (E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : Prop

A map is completely copositive if composing it with transposition gives a completely positive map.

This is the convention used in Wolf Chapter 3: a decomposable positive map is written as a completely positive map plus a map F for which F ∘ transpose is completely positive.

Equations

• IsCompletelyCopositiveMap E = IsCPMap (E ∘ₗ Matrix.transposeLinearMapComplex n)

def IsDecomposablePositiveMap {n : Type u_1} [Fintype n] (E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : Prop

A decomposable positive map is a sum of a completely positive map and a completely copositive map. This is the class used in Wolf Chapter 3 to describe positive maps that cannot detect PPT entanglement.

Equations

• IsDecomposablePositiveMap E = ∃ (Ecp : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) (Eccp : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ), IsCPMap Ecp ∧ IsCompletelyCopositiveMap Eccp ∧ E = Ecp + Eccp

def IsIndecomposablePositiveMap {n : Type u_1} [Fintype n] (E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : Prop

An indecomposable positive map is positive but not decomposable.

Equations

• IsIndecomposablePositiveMap E = (IsPositiveMap E ∧ ¬IsDecomposablePositiveMap E)

theorem IsCPMap.isPositiveMap {n : Type u_1} [Fintype n] {E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (h : IsCPMap E) : IsPositiveMap E

A completely positive map is positive.

theorem IsCompletelyCopositiveMap.isPositiveMap {n : Type u_1} [Fintype n] {E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (h : IsCompletelyCopositiveMap E) : IsPositiveMap E

Completely copositive maps are positive.

theorem IsDecomposablePositiveMap.isPositiveMap {n : Type u_1} [Fintype n] {E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (h : IsDecomposablePositiveMap E) : IsPositiveMap E

Decomposable positive maps are positive.

theorem IsChannel.pos {n : Type u_1} [Fintype n] {E : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hE : IsChannel E) : IsPositiveMap E

A channel is a positive map (derived from complete positivity).

def IsPositiveMap.toPositiveLinearMap {m : Type u_1} {n : Type u_2} {E : Matrix n n ℂ →ₗ[ℂ] Matrix m m ℂ} (hE : IsPositiveMap E) : Matrix n n ℂ →ₚ[ℂ] Matrix m m ℂ

A positive matrix map is a positive linear map: if A ≤ B, then E A ≤ E B.

Equations

• hE.toPositiveLinearMap = { toLinearMap := E, monotone' := ⋯ }

theorem IsPositiveMap.map_isHermitian {m : Type u_1} {n : Type u_2} [Finite m] [Finite n] {E : Matrix n n ℂ →ₗ[ℂ] Matrix m m ℂ} (hE : IsPositiveMap E) {X : Matrix n n ℂ} (hX : X.IsHermitian) : (E X).IsHermitian

Positive maps preserve Hermiticity.

Density matrices: compactness and convexity

def densityMatrices (D : ℕ) : Set (Matrix (Fin D) (Fin D) ℂ)

The set of density matrices: PSD matrices with trace 1.

Equations

• densityMatrices D = {ρ : Matrix (Fin D) (Fin D) ℂ | ρ.PosSemidef ∧ ρ.trace = 1}

@[simp]

theorem mem_densityMatrices {D : ℕ} {ρ : Matrix (Fin D) (Fin D) ℂ} : ρ ∈ densityMatrices D ↔ ρ.PosSemidef ∧ ρ.trace = 1

Auxiliary lemmas for boundedness

Main results

theorem posSemidef_trace_bounded_isBounded {D : ℕ} (c : ℝ) : Bornology.IsBounded {X : Matrix (Fin D) (Fin D) ℂ | X.PosSemidef ∧ ‖X.trace‖ ≤ c}

PSD matrices with trace ≤ c form a bounded set (in the Frobenius norm).

For PSD X, every entry satisfies ‖X i j‖ ≤ ‖trace X‖ (diagonal: nonneg summand of trace; off-diagonal: Cauchy-Schwarz). Hence the sup-norm ‖X‖ ≤ ‖trace X‖ ≤ c.

theorem densityMatrices_isCompact {D : ℕ} : IsCompact (densityMatrices D)

The set of density matrices is compact (Heine-Borel).

Closed: intersection of the closed PSD cone and the closed set {trace = 1}. Bounded: PSD matrices with unit trace have bounded entries.

theorem densityMatrices_isConvex {D : ℕ} : Convex ℝ (densityMatrices D)

The set of density matrices is convex.

PSD cone is convex: a • ρ + b • σ is PSD when ρ, σ are PSD and a, b ≥ 0. Trace is linear: trace(a • ρ + b • σ) = a * 1 + b * 1 = 1 when a + b = 1.

theorem densityMatrices_nonempty {D : ℕ} (hD : 0 < D) : (densityMatrices D).Nonempty

The set of density matrices is nonempty when D > 0.

The matrix (1/D) • I is a density matrix.

Channels preserve density matrices

theorem IsChannel.map_densityMatrices {D : ℕ} (E : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ) (hE : IsChannel E) (ρ : Matrix (Fin D) (Fin D) ℂ) : ρ ∈ densityMatrices D → E ρ ∈ densityMatrices D

A channel (CPTP map) maps density matrices to density matrices.