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.

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 ρ passing 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.

theorem Sᵥₙ_eq_neg_trace_log {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : Sᵥₙ ρ = -inner ℝ (↑ρ).log ↑ρ

theorem Sᵥₙ_eq_trace_cfc_negMulLog {d : Type u_1} [Fintype d] [DecidableEq d] (ρ : MState d) : Sᵥₙ ρ = ((↑ρ).cfc Real.negMulLog).trace

Von Neumann entropy is the trace of the matrix function x ↦ -x log x.

@[simp]

theorem Sᵥₙ_unit_zero {d : Type u_1} [Fintype d] [DecidableEq d] [Unique d] (ρ : MState d) : Sᵥₙ ρ = 0

@[simp]

theorem Sᵥₙ_relabel {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ρ : MState d₁) (e : d₂ ≃ d₁) : Sᵥₙ (ρ.relabel e) = Sᵥₙ ρ

Von Neumann entropy is invariant under relabeling of the basis.

@[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.

@[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 selfAdjointMap_Continuous {𝕜 : Type u_11} [RCLike 𝕜] : Continuous ⇑IsMaximalSelfAdjoint.selfadjMap

theorem HermitianMat.trace_Continuous {d : Type u_11} {𝕜 : Type u_12} [Fintype d] [RCLike 𝕜] : Continuous trace

theorem Sᵥₙ_continuous {d : Type u_1} [Fintype d] [DecidableEq d] : Continuous Sᵥₙ

theorem traceLeft_eq_transpose_mul_conj {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂] (ψ : Ket (d₁ × d₂)) : ↑↑(MState.pure ψ).traceLeft = (vecToMat✝ ψ.vec).transpose * (vecToMat✝¹ ψ.vec).map star

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.

@[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.

@[simp]

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

For a pure state, the entropy of one subsystem equals the entropy of its complement, even after relabeling.