doc(Entropy): clarify relative entropy dependencies

Author: texra-ai

TNLean/Entropy/StrongSubadditivity.lean

@@ -47,7 +47,9 @@ Replace the sanctioned axiom `_root_.strong_subadditivity` (in
 `TNLean/Axioms/Entropy.lean`) with a proof along the classical route:
 1. Use `Entropy.quantumRelativeEntropy`, the trace-log relative entropy
    `D(ρ‖σ) = Re tr(ρ(log ρ − log σ))`.
-2. Establish Klein's inequality: `D(ρ‖σ) ≥ 0` for density matrices.
+2. Establish Klein's inequality: `D(ρ‖σ) ≥ 0` for density matrices with
+   positive definite reference state `σ` (and later the usual support condition
+   for singular `σ`).
 3. Lieb's joint concavity of `(A, B) ↦ tr(Kᴴ Aᵗ K B^{1-t})`.
 4. Monotonicity of the relative entropy under partial trace
    (the "data-processing inequality").

blueprint/src/chapter/ch19_entropy.tex

@@ -241,7 +241,8 @@ \section{Von Neumann entropy}
     \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}
+    \uses{def:quantum_relative_entropy, lem:quantum_relative_entropy_trace_split,
+        thm:entropy_eq_neg_trace_mul_log}
     If $\rho$ is Hermitian, then
     \[
         D(\rho\Vert\sigma)
@@ -250,9 +251,17 @@ \section{Von Neumann entropy}
 \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.
+    Apply Lemma~\ref{lem:quantum_relative_entropy_trace_split} to write
+    \[
+        D(\rho\Vert\sigma)
+            = \operatorname{Re}\operatorname{tr}(\rho\log\rho)
+              - \operatorname{Re}\operatorname{tr}(\rho\log\sigma).
+    \]
+    The trace-logarithm identity
+    \[
+        \operatorname{Re}\operatorname{tr}(\rho\log\rho)=-S(\rho)
+    \]
+    then gives the result.
 \end{proof}
 
 \begin{theorem}[Entropy is invariant under reindexing]