Concavity of the von Neumann entropy, and the Holevo quantity

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

• ★ vonNeumannEntropy_mixture_ge_of_posDef — concavity: for a finite mixture σ = ∑ᵢ pᵢ ρᵢ of density matrices with weights pᵢ ≥ 0 summing to one, ∑ᵢ pᵢ S(ρᵢ) ≤ S(σ), under Klein's full-support condition on σ. The condition is removed in ConcavityFull.lean (vonNeumannEntropy_mixture_ge), by mixing with the maximally mixed state and passing to the limit. The proof is the identity S(σ) − ∑ᵢ pᵢ S(ρᵢ) = ∑ᵢ pᵢ D(ρᵢ ‖ σ): the cross term Re Tr(σ log σ) is the p-average of Re Tr(ρᵢ log σ) (re_trace_finset_sum_smul_mul), and Klein's inequality (klein_inequality, Subadditivity.lean) bounds each by Re Tr(ρᵢ log ρᵢ) = −S(ρᵢ) (re_trace_self_log_eq_neg_vonNeumannEntropy);
• holevoChi — the Holevo quantity χ = S(∑ᵢ pᵢ ρᵢ) − ∑ᵢ pᵢ S(ρᵢ) of an ensemble, and ★ holevoChi_nonneg_of_posDef.

The full-support hypothesis is the same discipline as relEntropy_nonneg and vonNeumannEntropy_le_pinching: without it the junk value of log at 0 enters the cross term. ConcavityFull.lean removes it for concavity (and hence for holevoChi_nonneg) by continuity.

Consumers: CsdLean4/LF2/PreparationCoarseGraining.lean (coarse-graining a preparation on Σ does not decrease its entropy).

Concavity of the von Neumann entropy

theorem QuantumInfo.vonNeumannEntropy_congr_of_eq {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : A = B) : vonNeumannEntropy hA = vonNeumannEntropy hB

Von Neumann entropy depends only on the matrix (transport along an equality of matrices).

theorem QuantumInfo.re_trace_self_log_eq_neg_vonNeumannEntropy {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : RCLike.re (ρ * hρ.cfc Real.log).trace = -vonNeumannEntropy hρ

Re Tr(ρ log ρ) = −S(ρ).

theorem QuantumInfo.re_trace_finset_sum_smul_mul {n : Type u_1} [Fintype n] {ι : Type u_2} (s : Finset ι) (p : ι → ℝ) (ρ : ι → Matrix n n ℂ) (L : Matrix n n ℂ) : RCLike.re ((∑ i ∈ s, ↑(p i) • ρ i) * L).trace = ∑ i ∈ s, p i * RCLike.re (ρ i * L).trace

The cross term is affine in the first argument: for σ = ∑ᵢ pᵢ ρᵢ, Re Tr(σ L) = ∑ᵢ pᵢ Re Tr(ρᵢ L).

theorem QuantumInfo.vonNeumannEntropy_mixture_ge_of_posDef {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) (hpd : (∑ i : ι, ↑(p i) • ρ i).PosDef) : ∑ i : ι, p i * vonNeumannEntropy ⋯ ≤ vonNeumannEntropy ⋯

★ Concavity of the von Neumann entropy. For a finite mixture σ = ∑ᵢ pᵢ ρᵢ of density matrices with weights pᵢ ≥ 0 summing to one, and σ of full support (Klein's condition), ∑ᵢ pᵢ S(ρᵢ) ≤ S(σ). Proof: S(σ) − ∑ᵢ pᵢ S(ρᵢ) = ∑ᵢ pᵢ D(ρᵢ ‖ σ) ≥ 0 — the cross term Re Tr(σ log σ) is the p-average of Re Tr(ρᵢ log σ), and Klein's inequality bounds each by Re Tr(ρᵢ log ρᵢ) = −S(ρᵢ).

noncomputable def QuantumInfo.holevoChi {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (p : ι → ℝ) {ρ : ι → Matrix n n ℂ} (hρ : ∀ (i : ι), (ρ i).IsHermitian) (hσ : (∑ i : ι, ↑(p i) • ρ i).IsHermitian) : ℝ

The Holevo quantity χ = S(∑ᵢ pᵢ ρᵢ) − ∑ᵢ pᵢ S(ρᵢ) of an ensemble.

Equations

• QuantumInfo.holevoChi p hρ hσ = QuantumInfo.vonNeumannEntropy hσ - ∑ i : ι, p i * QuantumInfo.vonNeumannEntropy ⋯

theorem QuantumInfo.holevoChi_nonneg_of_posDef {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) (hpd : (∑ i : ι, ↑(p i) • ρ i).PosDef) : 0 ≤ holevoChi p ⋯ ⋯

★ The Holevo quantity is non-negative (concavity restated).