The Holevo bound and the single-letter Holevo range of a channel

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

Glossary: https://glossary.constraintsurfacedynamics.com/holevo-bound/ Plain-language, CSD-role and formal statements of the Holevo bound, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh. On upstreaming: this is a Category 1 file. Strip this Glossary block before any Mathlib or Physlib PR; a personal project link has no place in a canonical header.

• isHermitian_finset_sum_smul, posSemidef_finset_sum_smul, trace_finset_sum_smul_eq_one — a mixture of density matrices is a density matrix;
• holevoChi_le_vonNeumannEntropy, ★ holevoChi_le_log_card — the Holevo bound χ ≤ S(∑ᵢ pᵢ ρᵢ) ≤ log (dim), with no support hypothesis (only the non-negativity of the components' entropies is used);
• holevoRange Φ — the set of single-letter Holevo quantities of the outputs of a channel over all finite ensembles of density matrices, and ★ holevoRange_le_log_card: every one is at most log of the output dimension. The greatest element of holevoRange Φ, when it exists, is the single-letter Holevo capacity of Φ; CsdLean4/LF6/DeisolationCapacity.lean exhibits it for the de-isolation channel. The regularised classical capacity (many channel uses) is not defined here.

The Holevo bound (Cat-1)

theorem QuantumInfo.isHermitian_finset_sum_smul {n : Type u_1} {ι : Type u_2} (s : Finset ι) (p : ι → ℝ) {ρ : ι → Matrix n n ℂ} (hρ : ∀ (i : ι), (ρ i).IsHermitian) : (∑ i ∈ s, ↑(p i) • ρ i).IsHermitian

A real mixture of Hermitian matrices is Hermitian.

theorem QuantumInfo.posSemidef_finset_sum_smul {n : Type u_1} {ι : Type u_2} (s : Finset ι) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) {ρ : ι → Matrix n n ℂ} (hρ : ∀ (i : ι), (ρ i).PosSemidef) : (∑ i ∈ s, ↑(p i) • ρ i).PosSemidef

A mixture of positive semidefinite matrices with non-negative weights is positive semidefinite.

theorem QuantumInfo.trace_finset_sum_smul_eq_one {n : Type u_1} [Fintype n] {ι : Type u_2} [Fintype ι] (p : ι → ℝ) (hp1 : ∑ i : ι, p i = 1) {ρ : ι → Matrix n n ℂ} (htr : ∀ (i : ι), (ρ i).trace = 1) : (∑ i : ι, ↑(p i) • ρ i).trace = 1

The trace of a mixture of trace-one matrices with weights summing to one is one.

theorem QuantumInfo.holevoChi_le_vonNeumannEntropy {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) {ρ : ι → Matrix n n ℂ} (hρ : ∀ (i : ι), (ρ i).PosSemidef) (htr : ∀ (i : ι), (ρ i).trace = 1) (hσ : (∑ i : ι, ↑(p i) • ρ i).IsHermitian) : holevoChi p ⋯ hσ ≤ vonNeumannEntropy hσ

The Holevo quantity is at most the entropy of the average state.

theorem QuantumInfo.holevoChi_le_log_card {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hp1 : ∑ i : ι, p i = 1) {ρ : ι → Matrix n n ℂ} (hρ : ∀ (i : ι), (ρ i).PosSemidef) (htr : ∀ (i : ι), (ρ i).trace = 1) (hσ : (∑ i : ι, ↑(p i) • ρ i).IsHermitian) : holevoChi p ⋯ hσ ≤ Real.log ↑(Fintype.card n)

★ The Holevo bound: χ ≤ log (dim).

def QuantumInfo.holevoRange {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} {ι' : Type u_3} [Fintype m] [Fintype ι'] [DecidableEq m] (Φ : Channel n m ι') : Set ℝ

The single-letter Holevo range of a channel: the Holevo quantities of the channel outputs of all finite ensembles of density matrices. Its greatest element, when it exists, is the single-letter Holevo capacity.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumInfo.holevoRange_le_log_card {n : Type u_1} [Fintype n] [DecidableEq n] {m : Type u_2} {ι' : Type u_3} [Fintype m] [Fintype ι'] [DecidableEq m] (Φ : Channel n m ι') {x : ℝ} (hx : x ∈ holevoRange Φ) : x ≤ Real.log ↑(Fintype.card m)

★ Every single-letter Holevo quantity of a channel is at most log (dim) of the output.