Conditional quantum entropy
import Quantum_entropy variables (ℋ₁ ℋ₂ : Type) [complex_Hilbert_space ℋ₁] [complex_Hilbert_space ℋ₂] (ρ : ℋ₁⊗ℋ₂ →ₗ[∁] ℋ₁⊗ℋ₂) [quantum_state ρ] def cond_quantum_entropy [quantum_state ρ] : ℝ := quantum_entropy ρ - quantum_entropy (pTr_1 ρ) notation `H(`A`|`B`)_`ρ := cond_quantum_entropy (ρ)
“Alice and Bob share n copies of ρAB qubit pairs. Large n.
free access to classical side channel. We count the number of times that they use a noiseless qubit channel.
Alice would like to send Bob qubits over a noiseless qubit channel so that he receives her share of the state ρAB.
The naive approach: Alice uses the channel n times to send her n shares.
theorem Alice_can_do_much_better :
cond_quantum_entropy ρAB > 0,
Alice needs to use the channel only `≈ nH(A|B)` times :=
sorry
Conditional quantum entropy can be negative. If so, then Alice does not need to use the noiseless qubit channel at all, and at the end of the protocol, Alice and Bob share ≈ nH(A|B) noiseless ebits!
They can then use these ebits for future communication purposes, such as a Quantum teleportation or super-dense coding protocol.
negative Conditional quantum entropy: potential for quantum communication.”