feat(Analysis/Entropy): add quantum relative entropy

Author: texra-ai

TNLean/Analysis/Entropy.lean

@@ -20,6 +20,7 @@ the basic quantum entropy infrastructure needed for MPDO / RFP applications.
 ## Main definitions
 
 * `vonNeumannEntropy`: `S(ρ) = ∑ᵢ negMulLog(λᵢ)` where `λᵢ` are eigenvalues
+* `quantumRelativeEntropy`: `D(ρ‖σ) = Re tr(ρ(log ρ - log σ))`
 * `traceA_ABC`, `traceC_ABC`, `traceAC_ABC`: tripartite partial traces
 * `mutualInformation`: `I(A:B) = S(ρ_A) + S(ρ_B) - S(ρ_AB)`
 * `IsSSAEquality`: predicate for equality in strong subadditivity
@@ -143,6 +144,64 @@ theorem vonNeumannEntropy_eq_neg_trace_mul_log
   rw [htr, ← Finset.sum_neg_distrib]
   exact Finset.sum_congr rfl fun i _ => by simp only [Real.negMulLog]; ring
 
+open scoped Matrix.Norms.L2Operator in
+/-- **Quantum relative entropy**, in trace-log form.
+
+For matrices `ρ` and `σ` of the same finite dimension, this is the totalized
+trace-log expression
+`D(ρ‖σ) = Re tr(ρ · (log ρ - log σ))`, where the logarithm is `CFC.log`.
+When `ρ` is a density matrix and `σ` is positive definite, this is the usual
+finite-dimensional Umegaki relative entropy.
+
+The definition is total because Mathlib's `CFC.log` is total. The physical
+relative entropy domain is the positive semidefinite / positive definite one;
+outside that domain this declaration is only the algebraic trace-log expression.
+
+Source: standard; blueprint `def:quantum_relative_entropy`. -/
+noncomputable def quantumRelativeEntropy
+    (ρ σ : Matrix n n ℂ) : ℝ :=
+  (Matrix.trace (ρ * (CFC.log ρ - CFC.log σ))).re
+
+open scoped Matrix.Norms.L2Operator in
+/-- The trace-log form of relative entropy split into its two trace terms. -/
+theorem quantumRelativeEntropy_eq_trace_mul_log_sub
+    (ρ σ : Matrix n n ℂ) :
+    quantumRelativeEntropy ρ σ
+      = (Matrix.trace (ρ * CFC.log ρ)).re
+        - (Matrix.trace (ρ * CFC.log σ)).re := by
+  simp [quantumRelativeEntropy, Matrix.mul_sub, Matrix.trace_sub]
+
+open scoped Matrix.Norms.L2Operator in
+/-- A matrix has zero relative entropy with itself. -/
+@[simp] theorem quantumRelativeEntropy_self
+    (ρ : Matrix n n ℂ) :
+    quantumRelativeEntropy ρ ρ = 0 := by
+  simp [quantumRelativeEntropy]
+
+open scoped Matrix.Norms.L2Operator in
+/-- The zero left input has zero trace-log relative entropy. -/
+@[simp] theorem quantumRelativeEntropy_zero_left
+    (σ : Matrix n n ℂ) :
+    quantumRelativeEntropy 0 σ = 0 := by
+  simp [quantumRelativeEntropy]
+
+open scoped Matrix.Norms.L2Operator in
+/-- Relative entropy rewritten using the von Neumann entropy of the first
+argument.
+
+For Hermitian `ρ`,
+`D(ρ‖σ) = -S(ρ) - Re tr(ρ log σ)`. This is the representation used when
+relating the trace-log relative-entropy layer to the eigenvalue definition of
+von Neumann entropy. -/
+theorem quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log
+    {ρ σ : Matrix n n ℂ} (hρ : ρ.IsHermitian) :
+    quantumRelativeEntropy ρ σ
+      = -vonNeumannEntropy ρ hρ - (Matrix.trace (ρ * CFC.log σ)).re := by
+  rw [quantumRelativeEntropy_eq_trace_mul_log_sub]
+  have htrace : (Matrix.trace (ρ * CFC.log ρ)).re = -vonNeumannEntropy ρ hρ := by
+    linarith [vonNeumannEntropy_eq_neg_trace_mul_log hρ]
+  rw [htrace]
+
 /-- The von Neumann entropy depends only on the characteristic polynomial: it is
 the `negMulLog`-sum of the (real parts of the) roots of `charpoly`. -/
 theorem vonNeumannEntropy_eq_charpoly_roots (ρ : Matrix n n ℂ) (hρ : ρ.IsHermitian) :
@@ -337,7 +396,8 @@ theorem vonNeumannEntropy_le_log_rank
   rw [hLHS] at hJensen
   -- `k⁻¹ · S ≤ negMulLog(k⁻¹) = k⁻¹ · log k`, multiply by `k`
   have hrhs : (k : ℝ) * Real.negMulLog ((k : ℝ)⁻¹) = Real.log k := by
-    rw [Real.negMulLog, Real.log_inv, neg_mul_neg, ← mul_assoc, mul_inv_cancel₀ hkR.ne', one_mul]
+    rw [Real.negMulLog, Real.log_inv, neg_mul_neg, ← mul_assoc,
+      mul_inv_cancel₀ hkR.ne', one_mul]
   have hlhs : (k : ℝ) * ((k : ℝ)⁻¹ * vonNeumannEntropy ρ hρ.isHermitian)
       = vonNeumannEntropy ρ hρ.isHermitian := by
     rw [← mul_assoc, mul_inv_cancel₀ hkR.ne', one_mul]

TNLean/Entropy/StrongSubadditivity.lean

@@ -45,7 +45,8 @@ no duplicate axiomatization of SSA is introduced.
 
 Replace the sanctioned axiom `_root_.strong_subadditivity` (in
 `TNLean/Axioms/Entropy.lean`) with a proof along the classical route:
-1. Define quantum relative entropy `D(ρ‖σ) = tr(ρ(log ρ − log σ))`.
+1. Use `Entropy.quantumRelativeEntropy`, the trace-log relative entropy
+   `D(ρ‖σ) = Re tr(ρ(log ρ − log σ))`.
 2. Establish Klein's inequality: `D(ρ‖σ) ≥ 0` for density matrices.
 3. Lieb's joint concavity of `(A, B) ↦ tr(Kᴴ Aᵗ K B^{1-t})`.
 4. Monotonicity of the relative entropy under partial trace

TNLean/Entropy/VonNeumann.lean

@@ -34,6 +34,9 @@ with trivial unfolding `@[simp]` lemmas.
 * `Entropy.vonNeumannEntropy_le_log_dim` — alias of
   `_root_.vonNeumannEntropy_le_log_dim`: `S(ρ) ≤ log D` for density
   matrices on a `D`-dimensional system.
+* `Entropy.quantumRelativeEntropy` — alias of
+  `_root_.quantumRelativeEntropy`, the trace-log relative entropy
+  `D(ρ‖σ) = Re tr(ρ(log ρ - log σ))`.
 
 The aliases are definitionally equal to their `_root_` targets, so the
 two spellings are interchangeable in tactics; in particular no
@@ -75,4 +78,27 @@ alias vonNeumannEntropy_nonneg := _root_.vonNeumannEntropy_nonneg
 `_root_.vonNeumannEntropy_le_log_dim`. -/
 alias vonNeumannEntropy_le_log_dim := _root_.vonNeumannEntropy_le_log_dim
 
+/-- **Quantum relative entropy**, namespaced alias of
+`_root_.quantumRelativeEntropy`. -/
+noncomputable alias quantumRelativeEntropy := _root_.quantumRelativeEntropy
+
+/-- Trace-log splitting formula for quantum relative entropy, namespaced alias
+of `_root_.quantumRelativeEntropy_eq_trace_mul_log_sub`. -/
+alias quantumRelativeEntropy_eq_trace_mul_log_sub :=
+  _root_.quantumRelativeEntropy_eq_trace_mul_log_sub
+
+/-- A matrix has zero relative entropy with itself, namespaced alias of
+`_root_.quantumRelativeEntropy_self`. -/
+alias quantumRelativeEntropy_self := _root_.quantumRelativeEntropy_self
+
+/-- The zero left input has zero trace-log relative entropy, namespaced alias of
+`_root_.quantumRelativeEntropy_zero_left`. -/
+alias quantumRelativeEntropy_zero_left := _root_.quantumRelativeEntropy_zero_left
+
+/-- Relative entropy rewritten using the von Neumann entropy of the first
+argument, namespaced alias of
+`_root_.quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log`. -/
+alias quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log :=
+  _root_.quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log
+
 end Entropy

blueprint/src/chapter/ch19_entropy.tex

@@ -177,6 +177,84 @@ \section{Von Neumann entropy}
     standard expression $S(\rho) = -\operatorname{tr}(\rho\log\rho)$.
 \end{remark}
 
+\begin{definition}[Quantum relative entropy]\label{def:quantum_relative_entropy}
+    \lean{quantumRelativeEntropy}
+    \leanok
+    For matrices $\rho,\sigma\in \MN{D}$, define the trace-log expression
+    \[
+        D(\rho\Vert\sigma)
+            = \operatorname{Re}\operatorname{tr}\bigl(\rho(\log\rho-\log\sigma)\bigr).
+    \]
+    On the physical domain where $\rho$ is a density matrix and $\sigma$ is
+    positive definite, this is the Umegaki relative entropy.
+\end{definition}
+
+\begin{lemma}[Trace-log splitting for relative entropy]
+    \label{lem:quantum_relative_entropy_trace_split}
+    \lean{quantumRelativeEntropy_eq_trace_mul_log_sub}
+    \leanok
+    \uses{def:quantum_relative_entropy}
+    For matrices $\rho,\sigma\in \MN{D}$,
+    \[
+        D(\rho\Vert\sigma)
+            = \operatorname{Re}\operatorname{tr}(\rho\log\rho)
+              - \operatorname{Re}\operatorname{tr}(\rho\log\sigma).
+    \]
+\end{lemma}
+
+\begin{proof}\leanok
+    Expand the matrix product over the difference $\log\rho-\log\sigma$ and use
+    linearity of the trace and of the real part.
+\end{proof}
+
+\begin{lemma}[Relative entropy with identical arguments]
+    \label{lem:quantum_relative_entropy_self}
+    \lean{quantumRelativeEntropy_self}
+    \leanok
+    \uses{def:quantum_relative_entropy}
+    For every matrix $\rho\in \MN{D}$,
+    \[
+        D(\rho\Vert\rho)=0.
+    \]
+\end{lemma}
+
+\begin{proof}\leanok
+    The logarithmic difference $\log\rho-\log\rho$ vanishes.
+\end{proof}
+
+\begin{lemma}[Relative entropy with zero first argument]
+    \label{lem:quantum_relative_entropy_zero_left}
+    \lean{quantumRelativeEntropy_zero_left}
+    \leanok
+    \uses{def:quantum_relative_entropy}
+    For every matrix $\sigma\in \MN{D}$,
+    \[
+        D(0\Vert\sigma)=0.
+    \]
+\end{lemma}
+
+\begin{proof}\leanok
+    The trace-log expression is multiplied on the left by the zero matrix.
+\end{proof}
+
+\begin{theorem}[Relative entropy in entropy form]
+    \label{thm:quantum_relative_entropy_entropy_form}
+    \lean{quantumRelativeEntropy_eq_neg_entropy_sub_trace_mul_log}
+    \leanok
+    \uses{def:quantum_relative_entropy, thm:entropy_eq_neg_trace_mul_log}
+    If $\rho$ is Hermitian, then
+    \[
+        D(\rho\Vert\sigma)
+            = -S(\rho)-\operatorname{Re}\operatorname{tr}(\rho\log\sigma).
+    \]
+\end{theorem}
+
+\begin{proof}\leanok
+    Split the definition of $D(\rho\Vert\sigma)$ into its two trace terms and
+    replace the first term by $-S(\rho)$ using the trace-logarithm form of the
+    von Neumann entropy.
+\end{proof}
+
 \begin{theorem}[Entropy is invariant under reindexing]
     \label{thm:entropy_submatrix_equiv}
     \lean{vonNeumannEntropy_submatrix_equiv}
@@ -398,7 +476,8 @@ \section{Entropy formulations}
 standard entropy literature and supply the entropy-theoretic input for the
 later MPDO arguments.
 
-\begin{definition}[Entropy formulation of von Neumann entropy]\label{def:entropy_von_neumann_entropy}
+\begin{definition}[Entropy formulation of von Neumann entropy]
+    \label{def:entropy_von_neumann_entropy}
     \lean{Entropy.vonNeumannEntropy}
     \leanok
     \uses{def:von_neumann_entropy}