Entanglement cost of quantum channel

How to simulate m ideal channels with n uses of a noisy quantum channel 𝒩? Equivalently: How to create m ideal Bell pairs with n uses of 𝒩?

In the limit of large n, the rate m/n defines the channel’s Capacity for quantum communication.

“The question upside down: What is the optimal rate at which a perfect channel can simulate a noisy one? At what rate are Bell pairs needed to asymptotically simulate 𝒩?”

import Quantum_channel
import Entanglement_of_formation_of_quantum_state

/--
"The entanglement cost of a quantum channel 𝒩
is the minimal rate at which entanglement is needed 
to simulate many copies of 𝒩, 
assuming classical communication is free."
-/
def entanglment_cost [quantum_channel 𝒩] : ℝ := sorry

theorem entanglement_cost_of_quantum_channel_eq_reg_max_entanglement_of_formation :
entanglement_cost 𝒩 = lim n→∞ 1/n * max {entanglement_of_formation((𝒩^⊗n ⊗ 1) ψⁿ) | pure ψⁿ} :=
sorry

Lower bounds on entanglement cost of quantum channel;

May be related to Emulate isometry with LOCC:

“Def 10. Consider a bipartite system with parties Alice and Bob. Let ε ≥ 0, Φ be a maximally entangled state between Alice and Bob, and quantum_channel 𝒩.”

import LOCC
import Diamond_distance_between_quantum_channels

-- "A one-shot channel simulation for 𝒩 with error ε is a quantum protocol:"

def simulation_map (ρ) [LOCC Λ] := λ ρ, Λ(ρ ⊗ Φ)

def one_shot_channel_simulation (ℱ) (ε) (𝒩) := ∥Λ(ρ ⊗ Φ) - 𝒩∥⋄ ≤ ε

"This condition assures that ∀ ρ, 
ℱ(ρ) can only distinguished with small probability from 𝒩(ρ)."

where Λ is a LOCC operation with no output at Alice’s side.

def entanglement_cost_one_shot_channel := log Schmidt_rank Φ

/--
"An asymptotic channel simulation for 𝒩 
is a sequence of one-shot channel simulations ℱn for 𝒩^⊗n with error εₙ, 
such that limn→∞ εₙ = 0."
-/
def asymptotic_channel_simulation (εₙ : ι → ℝ) [lim n→∞ εₙ = 0] (𝒩) := sorry

def entanglement_cost_asymptotic_channel_simulation := lim sup n→∞ log Rₙ/n

References