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.

structure PTPMap (dIn : Type u_1) (dOut : Type u_2) [Fintype dIn] [Fintype dOut] : Type (max u_1 u_2)

Positive trace-preserving linear maps. These includes all channels, but aren't necessarily completely positive, see CPTPMap.

• map : MatrixMap dIn dOut ℂ
• pos : self.map.IsPositive
• trace_preserving : self.map.IsTracePreserving

structure CPTPMap (dIn : Type u_1) (dOut : Type u_2) [Fintype dIn] [Fintype dOut] [DecidableEq dIn] extends PTPMap dIn dOut : Type (max u_1 u_2)

Quantum channels, aka CPTP maps: completely positive trace preserving linear maps. See CPTPMap.mk for a constructor that doesn't require going through PTPMap.

• mk' :: (
• map : MatrixMap dIn dOut ℂ
• pos : self.map.IsPositive
• trace_preserving : self.map.IsTracePreserving
• completely_pos : self.map.IsCompletelyPositive
• )

theorem PTPMap.ext {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {Λ₁ Λ₂ : PTPMap dIn dOut} (h : Λ₁.map = Λ₂.map) : Λ₁ = Λ₂

theorem PTPMap.apply_PosSemidef {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] {ρ : Matrix dIn dIn ℂ} (Λ : PTPMap dIn dOut) (hρ : ρ.PosSemidef) : (Λ.map ρ).PosSemidef

@[simp]

theorem PTPMap.apply_trace {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (Λ : PTPMap dIn dOut) (ρ : Matrix dIn dIn ℂ) : (Λ.map ρ).trace = ρ.trace

Simp lemma: the trace of the image of a PTPMap is the same as the original trace.

instance PTPMap.instFunLike {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] : FunLike (PTPMap dIn dOut) (MState dIn) (MState dOut)

Equations

• PTPMap.instFunLike = { coe := fun (Λ : PTPMap dIn dOut) (ρ : MState dIn) => { toSubtype := ⟨Λ.map ρ.m, ⋯⟩, zero_le := ⋯, tr := ⋯ }, coe_injective' := ⋯ }

theorem PTPMap.nonemptyOut {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] (Λ : PTPMap dIn dOut) [hIn : Nonempty dIn] [DecidableEq dIn] : Nonempty dOut

def CPTPMap.mk {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (map : MatrixMap dIn dOut ℂ) (tp : map.IsTracePreserving) (cp : map.IsCompletelyPositive) : CPTPMap dIn dOut

Construct a CPTPMap from the facts that it IsTracePreserving and IsCompletelyPositive.

Equations

• CPTPMap.mk map tp cp = { map := map, pos := ⋯, trace_preserving := tp, completely_pos := cp }

@[simp]

theorem CPTPMap.map_mk {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] (map : MatrixMap dIn dOut ℂ) (h₁ : map.IsTracePreserving) (h₂ : map.IsCompletelyPositive) : (mk map h₁ h₂).map = map

@[reducible]

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

The Choi matrix of a CPTPMap.

Equations

• Λ.choi = Λ.map.choi_matrix

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

Two CPTPMaps are equal if their projection to PTPMaps are equal.

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

Two CPTPMaps are equal if their MatrixMaps are equal.

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) : Λ.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 (dIn × dOut) (dIn × dOut) ℂ} (h₁ : M.PosSemidef) (h₂ : M.traceRight = 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₂ = CPTPMap.mk (MatrixMap.of_choi_matrix M) ⋯ ⋯

@[simp]

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

instance CPTPMap.instFunLike {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] : FunLike (CPTPMap dIn dOut) (MState dIn) (MState dOut)

CPTPMaps are functions from MStates to MStates.

Equations

• CPTPMap.instFunLike = { coe := fun (Λ : CPTPMap dIn dOut) (ρ : MState dIn) => Λ.toPTPMap ρ, coe_injective' := ⋯ }

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

theorem CPTPMap.ext {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] {Λ₁ Λ₂ : CPTPMap dIn dOut} (h : ∀ (ρ : 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

• Λ₂.compose Λ₁ = CPTPMap.mk (Λ₂.map ∘ₗ Λ₁.map) ⋯ ⋯

@[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] {Λ₁ : CPTPMap dIn dM} {Λ₂ : CPTPMap dM dOut} (ρ : MState dIn) : (Λ₂.compose Λ₁) ρ = Λ₂ (Λ₁ ρ)

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₂] (Λ₃ : CPTPMap dM₂ dOut) (Λ₂ : CPTPMap dM dM₂) (Λ₁ : CPTPMap dIn dM) : (Λ₃.compose Λ₂).compose Λ₁ = Λ₃.compose (Λ₂.compose Λ₁)

Composition of CPTPMaps is associative.

instance CPTPMap.instMixable {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] : Mixable (Matrix (dIn × dOut) (dIn × dOut) ℂ) (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 = CPTPMap.mk LinearMap.id ⋯ ⋯

@[simp]

theorem CPTPMap.id_fun_id {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] (M : Matrix dIn dIn ℂ) : id.map M = M

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.compose Λ = Λ

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) : Λ.compose id = Λ

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

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.

Equations

• CPTPMap.destroy = CPTPMap.CPTP_of_choi_PSD_Tr ⋯ ⋯

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 := ⋯ }

def CPTPMap.const_state {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [Unique dIn] (ρ : MState dOut) : CPTPMap dIn dOut

A state can be viewed as a CPTP map from the trivial Hilbert space (indexed by Unit) that outputs exactly that state.

Equations

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

@[simp]

theorem CPTPMap.const_state_apply {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [Unique dIn] (ρ : MState dOut) (ρ₀ : MState dIn) : (const_state ρ) ρ₀ = ρ

The output of const_state ρ is always that ρ.

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

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

Equations

• CPTPMap.replacement ρ = (CPTPMap.const_state ρ).compose CPTPMap.destroy

@[simp]

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

The output of replacement ρ is always that ρ.

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

• (Λ₁⊗Λ₂) = CPTPMap.mk (Λ₁.map.kron Λ₂.map) ⋯ ⋯

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

Equations

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

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 = CPTPMap.mk (MatrixMap.piKron fun (i : ι) => (Λi i).map) ⋯ ⋯

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.compose ((Λi 1).compose sorry)

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

• CPTPMap.traceLeft = sorry

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 = sorry

@[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.of_equiv {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.of_equiv σ = sorry

theorem CPTPMap.equiv_inverse {dIn : Type u_1} {dOut : Type u_2} [Fintype dIn] [Fintype dOut] [DecidableEq dIn] [DecidableEq dOut] (σ : dIn ≃ dOut) : ⇑(of_equiv σ) ∘ ⇑(of_equiv σ.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.of_equiv (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.of_equiv (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.of_equiv (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'

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.compose assoc' = id

def CPTPMap.of_unitary {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.of_unitary U = CPTPMap.CPTP_of_choi_PSD_Tr ⋯ ⋯

theorem CPTPMap.of_unitary_eq_conj {dIn : Type u_1} [Fintype dIn] [DecidableEq dIn] (U : ↥𝐔[dIn]) (ρ : MState dIn) : (of_unitary 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 of_unitary U.

Equations

• Λ.IsUnitary = ∃ (U : ↥𝐔[dIn]), Λ = CPTPMap.of_unitary 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) : (of_equiv σ).IsUnitary

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

A channel is entanglement breaking iff its product with the identity channel only outputs separable states.

Equations

• Λ.IsEntanglementBreaking = ∀ (dR : Type ?u.61) [inst : Fintype dR] [inst_1 : DecidableEq dR] (ρ : MState (dR × dIn)), ((CPTPMap.id⊗Λ) ρ).IsSeparable

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 = sorry

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) : Λ = let zero_prep := const_state (MState.pure (Ket.basis default)); let prep := id⊗zero_prep; let append := of_equiv (Equiv.prodPUnit dIn).symm; traceLeft.compose (traceLeft.compose (Λ.purify.compose (prep.compose 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

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

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.compose Λ = Λ₂

@[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)