Quantum notions of information and entropy.

We start with quantities of entropy, namely the von Neumann entropy and its derived quantities:

• Quantum conditional entropy, qConditionalEnt
• Quantum mutual information, qMutualInfo
• Coherent information, coherentInfo
• Quantum conditional mutual information, qcmi. and then prove facts about them.

The second half of the file is quantities of relative entropy, namely the (standard) quantum relative entropy, and generalizations.

def Sᵥₙ {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : ℝ

Von Neumann entropy of a mixed state.

Equations

• Sᵥₙ ρ = Hₛ ρ.spectrum

def qConditionalEnt {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : MState (dA × dB)) : ℝ

The Quantum Conditional Entropy S(ρᴬ|ρᴮ) is given by S(ρᴬᴮ) - S(ρᴮ).

Equations

• qConditionalEnt ρ = Sᵥₙ ρ - Sᵥₙ ρ.traceLeft

def qMutualInfo {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : MState (dA × dB)) : ℝ

The Quantum Mutual Information I(A:B) is given by S(ρᴬ) + S(ρᴮ) - S(ρᴬᴮ).

Equations

• qMutualInfo ρ = Sᵥₙ ρ.traceLeft + Sᵥₙ ρ.traceRight - Sᵥₙ ρ

def coherentInfo {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState d₁) (Λ : CPTPMap d₁ d₂ ℂ) : ℝ

The Coherent Information of a state ρ pasing through a channel Λ is the negative conditional entropy of the image under Λ of the purification of ρ.

Equations

• coherentInfo ρ Λ = -qConditionalEnt ((Λ⊗ₖCPTPMap.id) (MState.pure ρ.purify))

def qcmi {dA : Type u_5} {dB : Type u_6} {dC : Type u_7} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρ : MState (dA × dB × dC)) : ℝ

The Quantum Conditional Mutual Information, I(A;C|B) = S(A|B) - S(A|BC).

Equations

• qcmi ρ = qConditionalEnt ρ.assoc'.traceRight - qConditionalEnt ρ

theorem Sᵥₙ_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : 0 ≤ Sᵥₙ ρ

von Neumman entropy is nonnegative.

theorem Sᵥₙ_le_log_d {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : Sᵥₙ ρ ≤ Real.log ↑Finset.univ.card

von Neumman entropy is at most log d.

@[simp]

theorem Sᵥₙ_of_pure_zero {d : Type u_1} [Fintype d] [DecidableEq d] (ψ : Ket d) : Sᵥₙ (MState.pure ψ) = 0

von Neumman entropy of pure states is zero.

@[simp]

theorem Sᵥₙ_of_SWAP_eq {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : Sᵥₙ ρ.SWAP = Sᵥₙ ρ

von Neumann entropy is unchanged under SWAP. TODO: All unitaries

@[simp]

theorem Sᵥₙ_of_assoc_eq {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState ((d₁ × d₂) × d₃)) : Sᵥₙ ρ.assoc = Sᵥₙ ρ

von Neumann entropy is unchanged under assoc.

theorem Sᵥₙ_of_assoc'_eq {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ : MState (d₁ × d₂ × d₃)) : Sᵥₙ ρ.assoc' = Sᵥₙ ρ

von Neumann entropy is unchanged under assoc'.

theorem Sᵥₙ_of_partial_eq {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ψ : Ket (d₁ × d₂)) : Sᵥₙ (MState.pure ψ).traceLeft = Sᵥₙ (MState.pure ψ).traceRight

von Neumman entropies of the left- and right- partial trace of pure states are equal.

theorem Sᵥₙ_weak_monotonicity {dA : Type u_5} {dB : Type u_6} {dC : Type u_7} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρ : MState (dA × dB × dC)) : have ρAB := ρ.assoc'.traceRight; have ρAC := ρ.SWAP.assoc.traceLeft.SWAP; 0 ≤ qConditionalEnt ρAB + qConditionalEnt ρAC

Weak monotonicity of quantum conditional entropy. S(A|B) + S(A|C) ≥ 0

@[simp]

theorem qConditionalEnt_of_pure_symm {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ψ : Ket (d₁ × d₂)) : qConditionalEnt (MState.pure ψ).SWAP = qConditionalEnt (MState.pure ψ)

Quantum conditional entropy is symmetric for pure states.

@[simp]

theorem qMutualInfo_symm {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : qMutualInfo ρ.SWAP = qMutualInfo ρ

Quantum mutual information is symmetric.

theorem Sᵥₙ_subadditivity {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : Sᵥₙ ρ ≤ Sᵥₙ ρ.traceRight + Sᵥₙ ρ.traceLeft

"Ordinary" subadditivity of von Neumann entropy

theorem Sᵥₙ_triangle_subaddivity {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState (d₁ × d₂)) : |Sᵥₙ ρ.traceRight - Sᵥₙ ρ.traceLeft| ≤ Sᵥₙ ρ

Araki-Lieb triangle inequality on von Neumann entropy

theorem Sᵥₙ_strong_subadditivity {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ₁₂₃ : MState (d₁ × d₂ × d₃)) : have ρ₁₂ := ρ₁₂₃.assoc'.traceRight; have ρ₂₃ := ρ₁₂₃.traceLeft; have ρ₂ := ρ₁₂₃.traceLeft.traceRight; Sᵥₙ ρ₁₂₃ + Sᵥₙ ρ₂ ≤ Sᵥₙ ρ₁₂ + Sᵥₙ ρ₂₃

Strong subadditivity on a tripartite system

theorem qConditionalEnt_strong_subadditivity {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ₁₂₃ : MState (d₁ × d₂ × d₃)) : qConditionalEnt ρ₁₂₃ ≤ qConditionalEnt ρ₁₂₃.assoc'.traceRight

Strong subadditivity, stated in terms of conditional entropies. Also called the data processing inequality. H(A|BC) ≤ H(A|B).

theorem qMutualInfo_strong_subadditivity {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} [Fintype d₁] [Fintype d₂] [Fintype d₃] [DecidableEq d₁] [DecidableEq d₂] [DecidableEq d₃] (ρ₁₂₃ : MState (d₁ × d₂ × d₃)) : qMutualInfo ρ₁₂₃ ≥ qMutualInfo ρ₁₂₃.assoc'.traceRight

Strong subadditivity, stated in terms of quantum mutual information. I(A;BC) ≥ I(A;B).

theorem qcmi_nonneg {dA : Type u_5} {dB : Type u_6} {dC : Type u_7} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρ : MState (dA × dB × dC)) : 0 ≤ qcmi ρ

The quantum conditional mutual information QCMI is nonnegative.

theorem qcmi_le_2_log_dim {dA : Type u_5} {dB : Type u_6} {dC : Type u_7} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρ : MState (dA × dB × dC)) : qcmi ρ ≤ 2 * Real.log ↑(Fintype.card dA)

The quantum conditional mutual information QCMI ρABC is at most 2 log dA.

theorem qcmi_le_2_log_dim' {dA : Type u_5} {dB : Type u_6} {dC : Type u_7} [Fintype dA] [Fintype dB] [Fintype dC] [DecidableEq dA] [DecidableEq dB] [DecidableEq dC] (ρ : MState (dA × dB × dC)) : qcmi ρ ≤ 2 * Real.log ↑(Fintype.card dC)

The quantum conditional mutual information QCMI ρABC is at most 2 log dC.

To do relative entropies, we start with the sandwiched Renyi Relative Entropy which is a nice general form. Then instead of proving many theorems (like DPI, relabelling, additivity, etc.) several times, we just prove it for this one quantity, then it follows for other quantities (like the relative entropy) as a special case.

We could even imagine restructuring the file so that relative entropy comes first, then (some) properties about other quantities can be derived, since they can pretty much all be expressed in terms of appropriate special cases of relative entropies.

def SandwichedRelRentropy {d : Type u_1} [DecidableEq d] [Fintype d] (α : ℝ) (ρ σ : MState d) : ENNReal

The Sandwiched Renyi Relative Entropy, defined with ln (nits). Note that at α = 1 this definition switch to the standard Relative Entropy, for continuity.

Equations

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

def «termD̃__(_‖_)» : Lean.ParserDescr

Equations

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

@[simp]

theorem sandwichedRelRentropy_additive {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (α : ℝ) (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) : D̃_α(ρ₁ ⊗ ρ₂‖σ₁ ⊗ σ₂) = D̃_α(ρ₁‖σ₁) + D̃_α(ρ₂‖σ₂)

The Sandwiched Renyi Relative entropy is additive when the inputs are product states

@[simp]

theorem sandwichedRelRentropy_relabel {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] {α : ℝ} (ρ σ : MState d) (e : d₂ ≃ d) : D̃_α(ρ.relabel e‖σ.relabel e) = D̃_α(ρ‖σ)

@[simp]

theorem sandwichedRelRentropy_self {d : Type u_10} [Fintype d] [DecidableEq d] {α : ℝ} (hα : 0 < α) (ρ : MState d) : D̃_α(ρ‖ρ) = 0

theorem sandwichedRelEntropy_ne_top {α : ℝ} {d : Type u_10} [Fintype d] [DecidableEq d] {ρ σ : MState d} (hσ : σ.m.PosDef) : D̃_α(ρ‖σ) ≠ ⊤

theorem sandwichedRelRentropy.continuousOn {d : Type u_10} [Fintype d] [DecidableEq d] (ρ σ : MState d) : ContinuousOn (fun (α : ℝ) => D̃_α(ρ‖σ)) (Set.Ioi 0)

theorem sandwichedRenyiEntropy_DPI {d : Type u_10} {d₂ : Type u_11} [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] {α : ℝ} (hα : 1 ≤ α) (ρ σ : MState d) (Φ : CPTPMap d d₂ ℂ) : D̃_α(Φ ρ‖Φ σ) ≤ D̃_α(ρ‖σ)

The Data Processing Inequality for the Sandwiched Renyi relative entropy. Proved in https://arxiv.org/pdf/1306.5920. Seems kind of involved.

def qRelativeEnt {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : ENNReal

The quantum relative entropy 𝐃(ρ‖σ) := Tr[ρ (log ρ - log σ)].

Equations

• 𝐃(ρ‖σ) = D̃_1(ρ‖σ)

def «term𝐃(_‖_)» : Lean.ParserDescr

Equations

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

theorem qRelativeEnt_ker {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} (h : (↑σ).ker ≤ (↑ρ).ker) : ↑𝐃(ρ‖σ) = ↑((↑ρ).inner ((↑ρ).log - (↑σ).log))

Quantum relative entropy as Tr[ρ (log ρ - log σ)] when supports are correct.

@[simp]

theorem qRelativeEnt_relabel {d : Type u_1} {d₂ : Type u_3} [Fintype d] [Fintype d₂] [DecidableEq d] [DecidableEq d₂] (ρ σ : MState d) (e : d₂ ≃ d) : 𝐃(ρ.relabel e‖σ.relabel e) = 𝐃(ρ‖σ)

The quantum relative entropy is unchanged by MState.relabel

theorem qRelativeEnt_op_le {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} {α : ℝ} (hpos : 0 < α) (h : ↑ρ ≤ α • ↑σ) : 𝐃(ρ‖σ) ≤ ENNReal.ofReal (Real.log α)

"Formula for conversion from operator inequality to quantum relative entropy", -- Proposition S17 of https://arxiv.org/pdf/2401.01926v2

theorem qRelEntropy_heq_congr {d₁ d₂ : Type u} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] {ρ₁ σ₁ : MState d₁} {ρ₂ σ₂ : MState d₂} (hd : d₁ = d₂) (hρ : ρ₁ ≍ ρ₂) (hσ : σ₁ ≍ σ₂) : 𝐃(ρ₁‖σ₁) = 𝐃(ρ₂‖σ₂)

theorem qRelativeEnt_rank {d : Type u_1} [Fintype d] [DecidableEq d] {ρ σ : MState d} (h : (↑σ).ker = ⊥) : ↑𝐃(ρ‖σ) = ↑((↑ρ).inner ((↑ρ).log - (↑σ).log))

Quantum relative entropy when σ has full rank

@[simp]

theorem qRelativeEnt_additive {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂) : 𝐃(ρ₁ ⊗ ρ₂‖σ₁ ⊗ σ₂) = 𝐃(ρ₁‖σ₁) + 𝐃(ρ₂‖σ₂)

The quantum relative entropy is additive when the inputs are product states

theorem qRelativeEnt.LowerSemicontinuous {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : _root_.LowerSemicontinuous fun (σ : MState d) => 𝐃(ρ‖σ)

Relative entropy is lower semicontinuous (in each argument, actually, but we only need in the latter here). Will need the fact that all the cfc / eigenvalue stuff is continuous, plus carefully handling what happens with the kernel subspace, which will make this a pain.

theorem qRelativeEnt_joint_convexity {d : Type u_1} [Fintype d] [DecidableEq d] (ρ₁ ρ₂ σ₁ σ₂ : MState d) (p : Prob) : 𝐃(p[ρ₁↔ρ₂]‖p[σ₁↔σ₂]) ≤ ↑↑p * 𝐃(ρ₁‖σ₁) + (1 - ↑↑p) * 𝐃(ρ₂‖σ₂)

Joint convexity of Quantum relative entropy. We can't state this with ConvexOn because that requires an AddCommMonoid, which MStates are not. Instead we state it with Mixable.

TODO:

• Add the Mixable instance that infers from the Coe so that the right hand side can be written as p [𝐃(ρ₁‖σ₁) ↔ 𝐃(ρ₂‖σ₂)]
• Define (joint) convexity as its own thing - a ConvexOn for Mixable types.
• Maybe, more broadly, find a way to make ConvexOn work with the subset of Matrix that corresponds to MState.

@[simp]

theorem qRelEntropy_self {d : Type u_10} [Fintype d] [DecidableEq d] (ρ : MState d) : 𝐃(ρ‖ρ) = 0

theorem qRelativeEnt_ne_top {d : Type u_10} [Fintype d] [DecidableEq d] {ρ σ : MState d} (hσ : σ.m.PosDef) : 𝐃(ρ‖σ) ≠ ⊤

theorem qMutualInfo_as_qRelativeEnt {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : MState (dA × dB)) : ↑(qMutualInfo ρ) = ↑𝐃(ρ‖ρ.traceRight ⊗ ρ.traceLeft)

I(A:B) = 𝐃(ρᴬᴮ‖ρᴬ ⊗ ρᴮ)

theorem qRelEntropy_le_add_of_le_smul {d : Type u_10} [Fintype d] [DecidableEq d] (ρ : MState d) {σ₁ σ₂ : MState d} (r : ℝ) (hσ : ↑σ₁ ≤ r • ↑σ₂) : 𝐃(ρ‖σ₁) ≤ 𝐃(ρ‖σ₂) + ENNReal.ofReal (Real.log r)