Capacity for private classical communication

“Alice selects message m from set 𝓜 of messages.

Alice prepares some Quantum state ρA′ₘⁿ as input to many uses of the Quantum channel 𝒩_{A′→B}. And transmits it.”

     ඌ            ============ ₁            O
    /|\                  ⋮                   /|\
                   ============ ₙ

Output state:     
𝒩_{A′ⁿ→Bⁿ}(ρA′ₘⁿ),                   

“Bob decodes Alice’s transmitted message m. With a POVM {Λₘ}.

-- probability of error
def pₑ(m) = Tr {(I − Λₘ) 𝒩_{A′ⁿ→Bⁿ}(ρA′ₘⁿ)},

-- maximal probability of error
def p∗ₑ := max m ∈ 𝓜 pₑ(m)

where p∗ₑ ≤ ε ∈ [0,1] for an (n,P,ε) code.

/-- code rate -/
def P := 1/n * log |𝓜|.

“Let U𝒩_{A′→BE} be an isometric extension of the channel 𝒩_{A′→B}.”

     ඌ            ============ ₁            O
    /|\                  ⋮                   /|\
                   ============ ₙ                         
                   \     \
                    \ ... \      
                     \     \     
                         Ɋ
                         /|\

Eve receives:
𝒩ᶜ_{A′→E}(σ) := TrB{U𝒩_{A′→BE}(σ)}. 
/-- Eve’s state always close to constant state σEⁿ,
regardless of the message m Alice transmits. -/
def privacy (ε) : Prop :=
∀ m ∈ 𝓜, 1/2 * ‖ωEⁿₘ − σEⁿ‖₁ ≤ ε
import Quantum_channel

variables 
(𝒩 : (ℋ₁ →ₗ[∁] ℋ₁) →ₗ[∁] (ℋ₂ →ₗ[∁] ℋ₂)) [quantum_channel 𝒩]

/-- When can channel 𝒩 transmit at rate P? -/
def achievable_private_classical_comm_rate (P : ℝ) (𝒩) := 
∀ (ε > 0) (δ > 0), 
∃ k : ℕ, ∀ n ≥ k, 
∃ private_classical_comm_code (n,P−δ,ε)

/-- supremum of all achievable rates -/
def private_classical_capacity (𝒩) : ℝ :=
sup {P : ℝ | achievable_private_classical_comm_rate P 𝒩}

Private classical capacity of a channel is equal to its regularized private information

References