Local operation and classical communication

⇅ ==........== ⇅

“An LOCC Quantum channel consists of a finite number of compositions of measure-and-prepare actions”

Alice (or Bob) performs a Quantum instrument.


⇅   ඌ               ==........==                 o    ⇅
    /|\                                           /|\ 

She forwards the classical output to Bob.


 📞i ඌ               ==........==              📞i o 
    /|\                                           /|\

Bob performs a Quantum channel conditioned on the classical data received.


    ඌ               ==........==                 o    ⇅
    /|\                                           /|\ 

This sequence of actions corresponds to a channel ∑ x, (FA x) ⊗ (GB x), where {(FA x)} is a collection of completely positive maps such that ∑ x, (FA x) is a Quantum channel and {(GB x)} is a collection of Quantum channels.

/-- Local operations and classical communication. -/
def LOCC [quantum_channel Λ] := sorry

import Separable
import Partial_transpose

theorem LOCC_preserves_separable [quantum_state ρ] [LOCC Λ] :
separable ρ → separable (Λ ρ) := sorry

theorem LOCC_preserves_PPT [quantum_state ρ] [LOCC Λ] :
PPT ρ → PPT (Λ ρ) := sorry

lemma PPT_channel_of_LOCC [quantum_channel 𝒩] :
LOCC 𝒩 → PPT_channel 𝒩 := sorry

import Quantum_entropy

/-- A LOCC channel cannot create entanglement across any bipartite cut. -/
theorem entanglement_entropy_nonincreasing_after_LOCC [LOCC Λ] :
quantum_entropy Tr₂ Λ(ρ) ≤ quantum_entropy Tr₂ ρ := sorry

---

• LOCCs are Entanglement-breaking;

---

import Capacity_for_quantum_communication

theorem zero_quantum_capacity_of_LOCC [LOCC Λ] :
quantum_capacity Λ = 0 := sorry

References

• Wilde2011;