Completely Positive Trace Preserving maps

A CPTPMap is a ℂ-linear map between matrices (MatrixMap is an alias), bundled with the facts that it IsCompletelyPositive and IsTracePreserving. CPTP maps are typically regarded as the "most general quantum operation", as they map density matrices (MStates) to density matrices. The type PTPMap, for maps that are positive (but not necessarily completely positive) is also declared.

A large portion of the theory is in terms of the Choi matrix (MatrixMap.choi_matrix), as the positive-definiteness of this matrix corresponds to being a CP map. This is Choi's theorem on CP maps.

This file also defines several important examples of, classes of, and operations on, CPTPMaps:

• compose: Composition of maps
• id: The identity map
• replacement: The replacement channel that always outputs the same state
• prod: Tensor product of two CPTP maps, with notation M₁ ⊗ M₂
• piProd: Tensor product of finitely many CPTP maps (Pi-type product)
• of_unitary: The CPTP map corresponding to a unitary opeation U
• IsUnitary: Predicate whether the map corresponds to any unitary
• purify: Purifying a channel into a unitary on a larger Hilbert space
• complementary: The complementary channel to its purification
• IsEntanglementBreaking, IsDegradable, IsAntidegradable: Entanglement breaking, degradable and antidegradable channels.
• SWAP, assoc, assoc', traceLeft, traceRight: The CPTP maps corresponding to important operations on states. These correspond directly to MState.SWAP, MState.assoc, MState.assoc', MState.traceLeft, and MState.traceRight.

@[reducible]

def CPTPMap.choi {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (Λ : CPTPMap dIn dOut ℂ) : Matrix (dOut × dIn) (dOut × dIn) ℂ

The Choi matrix of a CPTPMap.

Equations

• Λ.choi = (((Λ.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map.choi_matrix

theorem CPTPMap.choi_ext {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] {Λ₁ Λ₂ : CPTPMap dIn dOut ℂ} (h : Λ₁.choi = Λ₂.choi) : Λ₁ = Λ₂

Two CPTPMaps are equal if their Choi matrices are equal.

theorem CPTPMap.choi_PSD_of_CPTP {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (Λ : CPTPMap dIn dOut ℂ) : (((Λ.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map.choi_matrix.PosSemidef

The Choi matrix of a channel is PSD.

@[simp]

theorem CPTPMap.Tr_of_choi_of_CPTP {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (Λ : CPTPMap dIn dOut ℂ) : Λ.choi.trace = ↑Finset.univ.card

The trace of a Choi matrix of a CPTP map is the cardinality of the input space.

def CPTPMap.CPTP_of_choi_PSD_Tr {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] {M : Matrix (dOut × dIn) (dOut × dIn) ℂ} (h₁ : M.PosSemidef) (h₂ : M.traceLeft = 1) : CPTPMap dIn dOut ℂ

Construct a CPTP map from a PSD Choi matrix with correct partial trace.

Equations

• CPTPMap.CPTP_of_choi_PSD_Tr h₁ h₂ = { toLinearMap := MatrixMap.of_choi_matrix M, HP := ⋯, pos := ⋯, TP := ⋯, cp := ⋯ }

@[simp]

theorem CPTPMap.choi_of_CPTP_of_choi {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (M : Matrix (dOut × dIn) (dOut × dIn) ℂ) {h₁ : M.PosSemidef} {h₂ : M.traceLeft = 1} : (CPTP_of_choi_PSD_Tr h₁ h₂).choi = M

theorem CPTPMap.mat_coe_eq_apply_mat {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (Λ : CPTPMap dIn dOut ℂ) [DecidableEq dOut] (ρ : MState dIn) : (Λ ρ).m = (((Λ.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map ρ.m

theorem CPTPMap.funext {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] {Λ₁ Λ₂ : CPTPMap dIn dOut ℂ} (h : ∀ (ρ : MState dIn), Λ₁ ρ = Λ₂ ρ) : Λ₁ = Λ₂

theorem CPTPMap.funext_iff {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] {Λ₁ Λ₂ : CPTPMap dIn dOut ℂ} : Λ₁ = Λ₂ ↔ ∀ (ρ : MState dIn), Λ₁ ρ = Λ₂ ρ

def CPTPMap.compose {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] {dM : Type u_4} [Fintype dM] [DecidableEq dM] (Λ₂ : CPTPMap dM dOut ℂ) (Λ₁ : CPTPMap dIn dM ℂ) : CPTPMap dIn dOut ℂ

The composition of CPTPMaps, as a CPTPMap.

Equations

• Λ₂∘ₘΛ₁ = { toLinearMap := (((Λ₂.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map ∘ₗ (((Λ₁.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map, HP := ⋯, pos := ⋯, TP := ⋯, cp := ⋯ }

def CPTPMap.«term_∘ₘ_» : Lean.TrailingParserDescr

Equations

• CPTPMap.«term_∘ₘ_» = Lean.ParserDescr.trailingNode `CPTPMap.«term_∘ₘ_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∘ₘ") (Lean.ParserDescr.cat `term 76))

@[simp]

theorem CPTPMap.compose_eq {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] {dM : Type u_4} [Fintype dM] [DecidableEq dM] [DecidableEq dOut] {Λ₁ : CPTPMap dIn dM ℂ} {Λ₂ : CPTPMap dM dOut ℂ} (ρ : MState dIn) : (Λ₂∘ₘΛ₁) ρ = Λ₂ (Λ₁ ρ)

Composition of CPTPMaps by CPTPMap.compose is compatible with the instFunLike action.

theorem CPTPMap.compose_assoc {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] {dM : Type u_4} [Fintype dM] [DecidableEq dM] {dM₂ : Type u_5} [Fintype dM₂] [DecidableEq dM₂] [DecidableEq dOut] (Λ₃ : CPTPMap dM₂ dOut ℂ) (Λ₂ : CPTPMap dM dM₂ ℂ) (Λ₁ : CPTPMap dIn dM ℂ) : Λ₃∘ₘΛ₂∘ₘΛ₁ = Λ₃∘ₘ(Λ₂∘ₘΛ₁)

Composition of CPTPMaps is associative.

instance CPTPMap.instMixable {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] : Mixable (Matrix (dOut × dIn) (dOut × dIn) ℂ) (CPTPMap dIn dOut ℂ)

CPTPMaps have a convex structure from their Choi matrices.

Equations

• One or more equations did not get rendered due to their size.

def CPTPMap.id {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] : CPTPMap dIn dIn ℂ

The identity channel, which leaves the input unchanged.

Equations

• CPTPMap.id = { toLinearMap := LinearMap.id, HP := ⋯, pos := ⋯, TP := ⋯, cp := ⋯ }

@[simp]

theorem CPTPMap.id_map {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] : (((id.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map = LinearMap.id

The map CPTPMap.id leaves any matrix unchanged.

@[simp]

theorem CPTPMap.id_MState {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] (ρ : MState dIn) : id ρ = ρ

The map CPTPMap.id leaves the input state unchanged.

@[simp]

theorem CPTPMap.id_compose {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (Λ : CPTPMap dIn dOut ℂ) : id∘ₘΛ = Λ

The map CPTPMap.id composed with any map is the same map.

@[simp]

theorem CPTPMap.compose_id {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (Λ : CPTPMap dIn dOut ℂ) : Λ∘ₘid = Λ

Any map composed with CPTPMap.id is the same map.

def CPTPMap.ofEquiv {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (σ : dIn ≃ dOut) : CPTPMap dIn dOut ℂ

Given a equivalence (a bijection) between the types d₁ and d₂, that is, if they're the same dimension, then there's a CPTP channel for this. This is what we need for defining e.g. the SWAP channel, which is 'unitary' but takes heterogeneous input and outputs types (d₁ × d₂) and (d₂ × d₁).

Equations

• CPTPMap.ofEquiv σ = { toLinearMap := MatrixMap.submatrix ℂ ⇑σ.symm, HP := ⋯, pos := ⋯, TP := ⋯, cp := ⋯ }

@[simp]

theorem CPTPMap.ofEquiv_apply {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (σ : dIn ≃ dOut) (ρ : MState dIn) : (ofEquiv σ) ρ = ρ.relabel σ.symm

@[simp]

theorem CPTPMap.equiv_inverse {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (σ : dIn ≃ dOut) : ⇑(ofEquiv σ) ∘ ⇑(ofEquiv σ.symm) = ⇑id

def CPTPMap.SWAP {d₁ : Type u_6} {d₂ : Type u_7} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] : CPTPMap (d₁ × d₂) (d₂ × d₁) ℂ

The SWAP operation, as a channel.

Equations

• CPTPMap.SWAP = CPTPMap.ofEquiv (Equiv.prodComm d₁ d₂)

def CPTPMap.assoc {d₁ : Type u_6} {d₂ : Type u_7} {d₃ : Type u_8} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] : CPTPMap ((d₁ × d₂) × d₃) (d₁ × d₂ × d₃) ℂ

The associator, as a channel.

Equations

• CPTPMap.assoc = CPTPMap.ofEquiv (Equiv.prodAssoc d₁ d₂ d₃)

def CPTPMap.assoc' {d₁ : Type u_6} {d₂ : Type u_7} {d₃ : Type u_8} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] : CPTPMap (d₁ × d₂ × d₃) ((d₁ × d₂) × d₃) ℂ

The inverse associator, as a channel.

Equations

• CPTPMap.assoc' = CPTPMap.ofEquiv (Equiv.prodAssoc d₁ d₂ d₃).symm

@[simp]

theorem CPTPMap.SWAP_eq_MState_SWAP {d₁ : Type u_6} {d₂ : Type u_7} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : SWAP ρ = ρ.SWAP

@[simp]

theorem CPTPMap.assoc_eq_MState_assoc {d₁ : Type u_6} {d₂ : Type u_7} {d₃ : Type u_8} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState ((d₁ × d₂) × d₃)) : assoc ρ = ρ.assoc

@[simp]

theorem CPTPMap.assoc'_eq_MState_assoc' {d₁ : Type u_6} {d₂ : Type u_7} {d₃ : Type u_8} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState (d₁ × d₂ × d₃)) : assoc' ρ = ρ.assoc'

@[simp]

theorem CPTPMap.assoc_assoc' {d₁ : Type u_6} {d₂ : Type u_7} {d₃ : Type u_8} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] : assoc∘ₘassoc' = id

def CPTPMap.traceLeft {d₁ : Type u_6} {d₂ : Type u_7} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] : CPTPMap (d₁ × d₂) d₂ ℂ

Partial tracing out the left, as a CPTP map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CPTPMap.traceLeft_toFun {d₁ : Type u_6} {d₂ : Type u_7} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (x : Matrix (d₁ × d₂) (d₁ × d₂) ℂ) : ((((traceLeft.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).toLinearMap ℂ).toFun x = x.traceLeft

def CPTPMap.traceRight {d₁ : Type u_6} {d₂ : Type u_7} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] : CPTPMap (d₁ × d₂) d₁ ℂ

Partial tracing out the right, as a CPTP map.

Equations

• CPTPMap.traceRight = CPTPMap.traceLeft∘ₘCPTPMap.SWAP

@[simp]

theorem CPTPMap.traceLeft_eq_MState_traceLeft {d₁ : Type u_6} {d₂ : Type u_7} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : traceLeft ρ = ρ.traceLeft

@[simp]

theorem CPTPMap.traceRight_eq_MState_traceRight {d₁ : Type u_6} {d₂ : Type u_7} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : traceRight ρ = ρ.traceRight

def CPTPMap.replacement {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [Nonempty dIn] [DecidableEq dOut] (ρ : MState dOut) : CPTPMap dIn dOut ℂ

The replacement channel that maps all inputs to a given state.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CPTPMap.replacement_apply {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [Nonempty dIn] [DecidableEq dOut] (ρ : MState dOut) (ρ₀ : MState dIn) : (replacement ρ) ρ₀ = ρ

The output of replacement ρ is always that ρ.

def CPTPMap.destroy {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [Nonempty dIn] [Unique dOut] : CPTPMap dIn dOut ℂ

There is a CPTP map that takes a system of any (nonzero) dimension and outputs the trivial Hilbert space, 1-dimensional, indexed by any Unique type. We can think of this as "destroying" the whole system; tracing out everything.

Equations

• CPTPMap.destroy = CPTPMap.replacement default

theorem CPTPMap.eq_if_output_unique {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [Unique dOut] (Λ₁ Λ₂ : CPTPMap dIn dOut ℂ) : Λ₁ = Λ₂

Two CPTP maps into the same one-dimensional output space must be equal

instance CPTPMap.instUnique {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [Nonempty dIn] [Unique dOut] : Unique (CPTPMap dIn dOut ℂ)

There is exactly one CPTPMap to a 1-dimensional space.

Equations

• CPTPMap.instUnique = { default := CPTPMap.destroy, uniq := ⋯ }

@[simp]

theorem CPTPMap.destroy_comp {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] {dOut₂ : Type u_6} [Unique dOut₂] [DecidableEq dOut] [Nonempty dIn] [Nonempty dOut] (Λ : CPTPMap dIn dOut ℂ) : destroy∘ₘΛ = destroy

def CPTPMap.prod {dI₁ : Type u_6} {dI₂ : Type u_7} {dO₁ : Type u_8} {dO₂ : Type u_9} [Fintype dI₁] [Fintype dI₂] [Fintype dO₁] [Fintype dO₂] [DecidableEq dI₁] [DecidableEq dI₂] (Λ₁ : CPTPMap dI₁ dO₁ ℂ) (Λ₂ : CPTPMap dI₂ dO₂ ℂ) : CPTPMap (dI₁ × dI₂) (dO₁ × dO₂) ℂ

The tensor product of two CPTPMaps.

Equations

• Λ₁⊗ₖΛ₂ = { toLinearMap := (((Λ₁.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map.kron (((Λ₂.toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map, HP := ⋯, pos := ⋯, TP := ⋯, cp := ⋯ }

def CPTPMap.«term_⊗ₖ_» : Lean.TrailingParserDescr

Equations

• CPTPMap.«term_⊗ₖ_» = Lean.ParserDescr.trailingNode `CPTPMap.«term_⊗ₖ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊗ₖ") (Lean.ParserDescr.cat `term 71))

def CPTPMap.piProd {ι : 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 : ι) → CPTPMap (dI i) (dO i) ℂ) : CPTPMap ((i : ι) → dI i) ((i : ι) → dO i) ℂ

Finitely-indexed tensor products of CPTPMaps.

Equations

• CPTPMap.piProd Λi = { toLinearMap := MatrixMap.piKron fun (i : ι) => ((((Λi i).toPTPMap ℂ).toPMap ℂ).toHPMap ℂ).map, HP := ⋯, pos := ⋯, TP := ⋯, cp := ⋯ }

theorem CPTPMap.fin_1_piProd {dI : Fin 1 → Type v} [Fintype (dI 0)] [DecidableEq (dI 0)] {dO : Fin 1 → Type w} [Fintype (dO 0)] [DecidableEq (dO 0)] (Λi : Fin 1 → CPTPMap (dI 0) (dO 0) ℂ) : piProd Λi = sorry∘ₘ(Λi 1∘ₘsorry)

def CPTPMap.ofUnitary {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] (U : ↥𝐔[dIn]) : CPTPMap dIn dIn ℂ

Conjugating density matrices by a unitary as a channel. This is standard unitary evolution.

Equations

• CPTPMap.ofUnitary U = { toLinearMap := MatrixMap.IsCompletelyPositive.conj ↑U, HP := ⋯, pos := ⋯, TP := ⋯, cp := ⋯ }

theorem CPTPMap.ofUnitary_eq_conj {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] (U : ↥𝐔[dIn]) (ρ : MState dIn) : (ofUnitary U) ρ = ρ.U_conj U

The unitary channel U conjugated by U.

def CPTPMap.IsUnitary {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] (Λ : CPTPMap dIn dIn ℂ) : Prop

A channel is unitary iff it is ofUnitary U.

Equations

• Λ.IsUnitary = ∃ (U : ↥𝐔[dIn]), Λ = CPTPMap.ofUnitary U

theorem CPTPMap.IsUnitary_iff_U_conj {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] (Λ : CPTPMap dIn dIn ℂ) : Λ.IsUnitary ↔ ∃ (U : ↥𝐔[dIn]), ∀ (ρ : MState dIn), Λ ρ = ρ.U_conj U

A channel is unitary iff it can be written as conjugation by a unitary.

theorem CPTPMap.IsUnitary_equiv {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] (σ : dIn ≃ dIn) : (ofEquiv σ).IsUnitary

def CPTPMap.purify {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (Λ : CPTPMap dIn dOut ℂ) : CPTPMap (dIn × dOut × dOut) (dIn × dOut × dOut) ℂ

Every channel can be written as a unitary channel on a larger system. In general, if the original channel was A→B, we may need to go as big as dilating the output system (the environment) by a factor of A*B. One way of stating this would be that it forms an isometry from A to (B×A×B). So that we can instead talk about the cleaner unitaries, we say that this is a unitary on (A×B×B). The defining properties that this is a valid purification comes are purify_IsUnitary and purify_trace. This means the environment always has type dIn × dOut.

Furthermore, since we need a canonical "0" state on B in order to add with the input, we require a typeclass instance [Inhabited dOut].

Equations

• Λ.purify = { toLinearMap := sorry, HP := ⋯, pos := ⋯, TP := ⋯, cp := ⋯ }

theorem CPTPMap.purify_IsUnitary {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] [Inhabited dOut] (Λ : CPTPMap dIn dOut ℂ) : Λ.purify.IsUnitary

theorem CPTPMap.purify_trace {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] [Inhabited dOut] (Λ : CPTPMap dIn dOut ℂ) : Λ = have zero_prep := replacement (MState.pure (Ket.basis default)); have prep := id⊗ₖzero_prep; have append := ofEquiv (Equiv.prodPUnit dIn).symm; traceLeft∘ₘtraceLeft∘ₘΛ.purify∘ₘprep∘ₘappend

With a channel Λ : A → B, a valid purification (A×B×B)→(A×B×B) is such that:

• Preparing the default ∣0⟩ state on two copies of B
• Appending these to the input
• Applying the purified unitary channel
• Tracing out the two left parts of the output is equivalent to the original channel. This theorem states that the channel output by purify has this property.

def CPTPMap.complementary {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] [Inhabited dOut] (Λ : CPTPMap dIn dOut ℂ) : CPTPMap dIn (dIn × dOut) ℂ

The complementary channel comes from tracing out the other half (the right half) of the purified channel purify.

Equations

• Λ.complementary = CPTPMap.traceRight∘ₘCPTPMap.assoc'∘ₘΛ.purify∘ₘ(CPTPMap.id⊗ₖCPTPMap.replacement (MState.pure (Ket.basis default)))∘ₘCPTPMap.ofEquiv (Equiv.prodPUnit dIn).symm

def CPTPMap.IsDegradableTo {dIn : Type u_1} {dOut : Type u_2} {dOut₂ : Type u_3} [Fintype dIn] [Fintype dOut] [Fintype dOut₂] [DecidableEq dIn] [DecidableEq dOut] (Λ : CPTPMap dIn dOut ℂ) (Λ₂ : CPTPMap dIn dOut₂ ℂ) : Prop

A channel is degradable to another, if the other can be written as a composition of a degrading channel D with the original channel.

Equations

• Λ.IsDegradableTo Λ₂ = ∃ (D : CPTPMap dOut dOut₂ ℂ), D∘ₘΛ = Λ₂

@[reducible]

def CPTPMap.IsAntidegradableTo {dIn : Type u_1} {dOut : Type u_2} {dOut₂ : Type u_3} [Fintype dIn] [Fintype dOut] [Fintype dOut₂] [DecidableEq dIn] [DecidableEq dOut₂] (Λ : CPTPMap dIn dOut ℂ) (Λ₂ : CPTPMap dIn dOut₂ ℂ) : Prop

A channel is antidegradable to another, if the other IsDegradableTo this one.

Equations

• Λ.IsAntidegradableTo Λ₂ = Λ₂.IsDegradableTo Λ

def CPTPMap.IsDegradable {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] [Inhabited dOut] (Λ : CPTPMap dIn dOut ℂ) : Prop

A channel is degradable if it IsDegradableTo its complementary channel.

Equations

• Λ.IsDegradable = Λ.IsDegradableTo Λ.complementary

@[reducible]

def CPTPMap.IsAntidegradable {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] [Inhabited dOut] (Λ : CPTPMap dIn dOut ℂ) : Prop

A channel is antidegradable if it IsAntidegradableTo its complementary channel.

Equations

• Λ.IsAntidegradable = Λ.IsAntidegradableTo Λ.complementary

instance CPTPMap.instTop {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] : TopologicalSpace (CPTPMap dIn dOut ℂ)

CPTPMaps inherit a topology from their choi matrices.

Equations

• CPTPMap.instTop = TopologicalSpace.induced CPTPMap.choi instTopologicalSpaceMatrix

theorem CPTPMap.choi_IsEmbedding {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] : Topology.IsEmbedding choi

The projection from CPTPMap to the Choi matrix is an embedding

instance CPTPMap.instT5MState {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] : T3Space (CPTPMap dIn dOut ℂ)