Concavity of the von Neumann entropy without the support hypothesis

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

Concavity.lean proves ∑ᵢ pᵢ S(ρᵢ) ≤ S(∑ᵢ pᵢ ρᵢ) under Klein's full-support condition on the mixture. This file removes it:

• mixOne A ε = (1 − ε) A + (ε / N) I — mixing with the maximally mixed state keeps density matrices density matrices (mixOne_posSemidef, mixOne_trace), makes them positive definite for ε > 0 (mixOne_posDef), commutes with mixtures (sum_smul_mixOne), and acts on the spectrum affinely, so its entropy is explicit: ★ vonNeumannEntropy_mixOne, S(mixOne A ε) = ∑ᵢ negMulLog ((1 − ε) λᵢ + ε / N) (via cfc_eq_conj_diagonal in the eigenbasis of A);
• ★ vonNeumannEntropy_mixture_ge — concavity with no support hypothesis: the supported inequality holds for the mixOnes at every ε ∈ (0, 1), both sides are continuous in ε, and the set where a continuous inequality holds is closed, so it holds at ε = 0;
• ★ holevoChi_nonneg — the Holevo quantity of any ensemble of density matrices is non-negative.

Consumers: CsdLean4/LF2/PreparationCoarseGraining.lean (mixing preparations on Σ), CsdLean4/Empirical/CSD/ChannelCapacity.lean (holevoChi2_nonneg).

Mixing with the maximally mixed state: explicit spectrum

noncomputable def QuantumInfo.mixOne {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) (ε : ℝ) : Matrix n n ℂ

A mixed with the maximally mixed state: (1 − ε) A + (ε / N) I.

Equations

• QuantumInfo.mixOne A ε = ↑(1 - ε) • A + ↑(ε / ↑(Fintype.card n)) • 1

theorem QuantumInfo.mixOne_zero {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℂ) : mixOne A 0 = A

theorem QuantumInfo.mixOne_isHermitian {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.IsHermitian) (ε : ℝ) : (mixOne A ε).IsHermitian

theorem QuantumInfo.mixOne_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosSemidef) {ε : ℝ} (h0 : 0 ≤ ε) (h1 : ε ≤ 1) : (mixOne A ε).PosSemidef

theorem QuantumInfo.mixOne_posDef {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosSemidef) {ε : ℝ} (h0 : 0 < ε) (h1 : ε ≤ 1) [Nonempty n] : (mixOne A ε).PosDef

theorem QuantumInfo.mixOne_trace {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (htr : A.trace = 1) (ε : ℝ) [Nonempty n] : (mixOne A ε).trace = 1

theorem QuantumInfo.sum_smul_mixOne {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (p : ι → ℝ) (hp1 : ∑ i : ι, p i = 1) (ρ : ι → Matrix n n ℂ) (ε : ℝ) : ∑ i : ι, ↑(p i) • mixOne (ρ i) ε = mixOne (∑ i : ι, ↑(p i) • ρ i) ε

The mixture of the mixOnes is the mixOne of the mixture.

theorem QuantumInfo.vonNeumannEntropy_mixOne {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.IsHermitian) (ε : ℝ) : vonNeumannEntropy ⋯ = ∑ i : n, ((1 - ε) * hA.eigenvalues i + ε / ↑(Fintype.card n)).negMulLog

The entropy of mixOne A ε is explicit: ∑ᵢ negMulLog ((1 − ε) λᵢ + ε / N) in the eigenvalues of A, since mixOne acts on the spectrum affinely (same eigenvectors).

Concavity without the support hypothesis

theorem QuantumInfo.vonNeumannEntropy_mixture_ge {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) : ∑ i : ι, p i * vonNeumannEntropy ⋯ ≤ vonNeumannEntropy ⋯

★ Concavity of the von Neumann entropy, no support hypothesis. For any finite mixture σ = ∑ᵢ pᵢ ρᵢ of density matrices with weights pᵢ ≥ 0 summing to one, ∑ᵢ pᵢ S(ρᵢ) ≤ S(σ). Proof: mix everything with the maximally mixed state, ρᵢ ↦ (1−ε) ρᵢ + (ε/N) I; the mixture is then positive definite and the supported version applies; both sides are explicit continuous functions of ε (vonNeumannEntropy_mixOne), so the inequality on (0, 1) passes to ε = 0 by closedness.

theorem QuantumInfo.holevoChi_nonneg {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) : 0 ≤ holevoChi p ⋯ ⋯

★ The Holevo quantity is non-negative, no support hypothesis.