Convert quantum state with catalyst
system S. in state ρ. can we Convert state to ρ’?
when does there exist a unitary on system S and system C (“catalyst”) so state of S changes from ρ to ρ’?
Entanglement transformations are irreversible under non-entangling operations.
/-- U brings ρ ε-close to ρ'. But leaves σ unchanged -/
def reachable_by_catalysis (ε : ℝ) [quantum_state ρ ρ'] :=
∃ [quantum_state σ] [unitary U],
D(Tr₂(U * (ρ ⊗ σ) * U†), ρ') ≤ ε
∧
Tr₁(U * (ρ ⊗ σ) * U†) = σ
notation ρ `→ε` ρ' := approx_cat_trans
/-- Thm. 2 -/
theorem reachable_by_catalysis_iff_higher_entropy :
(∀ ε>0, reachable_by_catalysis ε ρ ρ') ↔ H(ρ) ≤ H(ρ') :=
begin
split,
{ -- 1st direction: reachable_by_catalysis ρ ρ' → H(ρ) ≤ H(ρ')
-- U acts on ρ and σ
let ρσ' := U * (ρ ⊗ σ) * U†,
-- discard σ
let ρ'ε := Tr₂ ρσ',
calc H(ρ'ε) + H(σ) ≥ H(ρσ') -- entropy_subadditive
... = H(U * (ρ ⊗ σ) * U†) -- def of ρ'ε
... = H(ρ ⊗ σ) -- entropy_same_after_unitary
... = H(ρ) + H(σ) -- entropy_tmul_eq_add_entropy
-- so H(ρ'ε) ≥ H(ρ)
},
{ -- 2nd direction: H(ρ) ≤ H(ρ') → reachable_by_catalysis ρ ρ'
-- can reach ρ' using two catalysts
-- the first catalyst σ₁ consists of copies of S: S₂, ..., Sₙ and an auxiliary system A
let χ := U * ρ^⊗n * U†,
σ₁ = 1/n * ∑k, ρ^⊗{k-1} ⊗ χ{1,..,n-k} ⊗ |k⟩⟨k|A,
-- χ{1,..i} is χ reduced on subsystems 1 to i.
-- We define χ₀ = ρ^⊗⁰ = 1.
/- do unitaries on ρ ⊗ σ₁:
U₁ := U ⊗ |n⟩⟨n| + 1 ⊗ ∑k, |k⟩⟨k|, with U the unitary from lemma 5.
U₂ := cyclic shift of subsystems Sᵢ → Sᵢ₊₁ with Sₙ → S₁.
U₃ := cyclic shift on A, acting on |i⟩ → |i+1⟩ with |n+1⟩ = |1⟩ -/
let Uₜ := U₃ * U₂ * U₁,
/- The catalyst is back to σ₁ -/
have : Tr₁(Uₜ * (ρ ⊗ σ₁) * Uₜ†) = σ₁, { sorry },
/- System S is in χ' := 1/n * ∑ k, χₖ -- where χₖ = pTr_k' χ -/
have : Tr₂(Uₜ * (ρ ⊗ σ₁) * Uₜ†) = χ', { sorry },
-- the second catalyst is a src of randomness R
-- dilates the dephasing on S so correlates not to S₂, ..., Sₙ and A
-- After dephasing with R:
have : D(1/n * ∑ k, 𝒟 ρ'[χₖ], ρ') ≤ ε, {
D(1/n * ∑ k, 𝒟 ρ'[χₖ], ρ') ≤ 1/n ∑ k, D(𝒟 ρ'[χₖ], ρ') -- by triangle ineq
... ≤ ε -- by Lemma 5
},
},
end
/-- mixed unitary channel -/
def 𝒞 (ρ) [rnd_var p] [V : ι → unitary] :=
∑ i, pᵢ * Vᵢ * ρ * Vᵢ†
/-- dilated mixed unitary channel -/
def σ := ∑ i, pᵢ |i⟩⟨i|
def V := ∑ i, Vᵢ ⊗ |i⟩⟨i|
def 𝒞'(ρ) = Tr₂[V * (ρ ⊗ σ) * V†]
/-- Lemma 6: dilation catalyst does not correlate with an auxiliary system S' -/
lemma dilation_catalyst_correlates_not :
TrS[(V ⊗ 1S') ρSS' ⊗ σ (V† ⊗ 1S')] = ρS' ⊗ σ
begin
calc TrS[(V ⊗ 1S') ρSS' ⊗ σ (V† ⊗ 1S')] = TrS[ρSS' ⊗ σ] -- trace_unitary_invariant
... = ρS' ⊗ σ
end
def dephasing_channel_in_eigenbasis [quantum_state ρ] : quantum_channel := sorry
notation `𝒟` ρ := dephasing_channel_in_eigenbasis ρ
-- 𝒟 ρ' [ρ] = ∑ i, |i⟩⟨i| ρ |i⟩⟨i|
-- where |i⟩ is orthonormal basis of ρ'
/-- Lemma 5: "a candidate catalyst using Lemma 4"
upper bound on dist b/w target and dephasing on k-th copy of S -/
lemma basic_lemma [H(ρ) < H(ρ')] {ε > 0} :
∃ (n : ℕ) [unitary U], ∀ k ≤ n,
D(ρ', 𝒟 ρ' pTr_{1,..,n}\{k} (U * ρ^⊗n * U†))) ≤ ε
begin
have : ∃ (n : ℕ) [quantum_state ρ'εn], ρ^⊗n ≽ ρ'εn ∧ D(ρ'^⊗n, ρ'εn) ≤ ε, { sorry },
-- by Lemma 4 (uses H(ρ) < H(ρ'))
-- Schur-Horn theorem: ∃ U, ρ'εn = 𝒟 ρ'^⊗n [χ]
-- let k' := {1,...,n}\{k}
have : 𝒟 ρ' [χₖ] = Trk' [ρ'εn], {
-- By locality of quantum mechanics:
calc 𝒟 ρ' [χₖ] = Trk'[(𝒟 ρ' ⊗ 1k')[χ]]
... = Trk'[(𝒟 ρ'^⊗n)[χ]]
... = Trk'[ρ'εn]
},
have : D(ρ', 𝒟 ρ' [χₖ]) ≤ ε, {
calc D(ρ', 𝒟 ρ' [χₖ]) = D(ρ', Trk' [ρ'εn]) -- by this
... ≤ D(ρ', ρ'εn) -- nonincreasing under ptrace
... ≤ D(ρ'^⊗n, ρ'εn) -- nonincreasing under ptrace
... ≤ ε -- Lemma 4
},
end
consider more generally (ρ ρ’ : α →ₗ[ℂ] α).
when exists unitary from ρ to ρ’? when are they interconvertible?
what changes if we add the other axioms of quantum_state?