Quantum notions of information and entropy.

def Sᵥₙ {d : Type u_1} [Fintype 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] (ρ : 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] (ρ : 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₁] (ρ : 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 qRelativeEnt {d : Type u_1} [Fintype d] [DecidableEq d] (ρ σ : MState d) : ENNReal

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

Equations

• 𝐃(ρ‖σ) = if LinearMap.ker (Matrix.toLin' ↑σ.toSubtype) ≤ LinearMap.ker (Matrix.toLin' ↑ρ.toSubtype) then some ⟨(↑ρ).inner ((↑ρ).log - (↑σ).log), ⋯⟩ else ⊤

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 : LinearMap.ker (Matrix.toLin' ↑σ.toSubtype) ≤ LinearMap.ker (Matrix.toLin' ↑ρ.toSubtype)) : ↑𝐃(ρ‖σ) = ↑((↑ρ).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

def qcmi {dA : Type u_5} {dB : Type u_6} {dC : Type u_7} [Fintype dA] [Fintype dB] [Fintype 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 ρ

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.

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

Quantum relative entropy when σ has full rank

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_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 [qRelativeEnt ρ₁ σ₁ ↔ qRelativeEnt ρ₂ σ₂]
• 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.

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

von Neumman entropy is nonnegative.

theorem Sᵥₙ_le_log_d {d : Type u_1} [Fintype 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] (ψ : 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₂] (ρ : 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₂] (ρ : 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)) : let ρAB := ρ.assoc'.traceRight; let ρAC := ρ.SWAP.assoc.traceLeft.SWAP; 0 ≤ qConditionalEnt ρAB + qConditionalEnt ρAC

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

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 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 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) = S(AB‖ρᴬ⊗ρᴮ)

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₂] (ρ₁₂₃ : MState (d₁ × d₂ × d₃)) : let ρ₁₂ := ρ₁₂₃.assoc'.traceRight; let ρ₂₃ := ρ₁₂₃.traceLeft; let ρ₂ := ρ₁₂₃.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₂] (ρ₁₂₃ : 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₂] (ρ₁₂₃ : 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.

theorem qcmi_chain_rule {dB : Type u_6} {dC : Type u_7} {dA₁ : Type u_8} {dA₂ : Type u_9} [Fintype dB] [Fintype dC] [Fintype dA₁] [Fintype dA₂] [DecidableEq dB] [DecidableEq dC] [DecidableEq dA₁] [DecidableEq dA₂] (ρ : MState ((dA₁ × dA₂) × dB × dC)) : let ρA₁BC := ρ.assoc.SWAP.assoc.traceLeft.SWAP; let ρA₂BA₁C := ((CPTPMap.id⊗CPTPMap.assoc').compose (CPTPMap.assoc.compose (CPTPMap.SWAP⊗CPTPMap.id))) ρ; qcmi ρ = qcmi ρA₁BC + qcmi ρA₂BA₁C

The chain rule for quantum conditional mutual information: I(A₁A₂ : C | B) = I(A₁:C|B) + I(A₂:C|BA₁).