feat: add strong_subadditivity problem

LeanEval/Physics/StrongSubadditivity.lean

@@ -0,0 +1,53 @@
+import EvalTools.Markers
+import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
+import Mathlib.LinearAlgebra.Matrix.PosDef
+
+/-! # Strong subadditivity of quantum entropy
+
+States that `S(ρ_ABC) + S(ρ_B) ≤ S(ρ_AB) + S(ρ_BC)` where S is the von Neumann entropy.
+
+[Wikipedia article](https://en.wikipedia.org/wiki/Strong_subadditivity_of_quantum_entropy) on
+the significance of this inequality.
+
+-/
+
+namespace LeanEval
+namespace Physics
+
+variable {A B C : Type*}
+variable [Fintype A] [Fintype B] [Fintype C]
+variable [DecidableEq A] [DecidableEq B] [DecidableEq C]
+variable [Nonempty A] [Nonempty B] [Nonempty C]
+
+noncomputable section
+
+/-- Partial trace on the left of a matrix -/
+def _root_.Matrix.traceLeft (M : Matrix (A × B) (A × C) ℂ) : Matrix B C ℂ :=
+  Matrix.of fun i j ↦ ∑ k, M (k, i) (k, j)
+
+/-- Partial trace on the right of a matrix -/
+def _root_.Matrix.traceRight (M : Matrix (A × B) (C × B) ℂ) : Matrix A C ℂ :=
+  Matrix.of fun i j ↦ ∑ k, M (i, k) (j, k)
+
+/-- Von Neumann entropy of a quantum state -/
+def entropy (M : Matrix A A ℂ) : ℝ :=
+  -Complex.re (Matrix.trace (M * cfc Real.log M))
+
+open ComplexOrder
+
+/-- Strong subadditivity of quantum entropy. We relax the common assumption that M is a normalized
+ density matrix to the simpler statement that it's PSD, which holds since normalization just produces
+ a positive affine transformation on the entropy. -/
+@[eval_problem]
+theorem strong_subadditivity (M_ABC : Matrix (A × B × C) (A × B × C) ℂ) (h : M_ABC.PosSemidef) :
+    let M_AB : Matrix (A × B) (A × B) ℂ :=
+      .traceRight <| M_ABC.reindex (.symm <| .prodAssoc ..) (.symm <| .prodAssoc ..)
+    let M_BC : Matrix (B × C) (B × C) ℂ := M_ABC.traceLeft
+    let M_B : Matrix B B ℂ := M_BC.traceRight
+    entropy M_ABC + entropy M_B ≤ entropy M_AB + entropy M_BC := by
+  sorry
+
+end
+
+end Physics
+end LeanEval

manifests/problems/strong_subadditivity.toml

@@ -0,0 +1,9 @@
+id = "strong_subadditivity"
+title = "Strong Subadditivity of von Neumann Entropy"
+test = false
+module = "LeanEval.Physics.StrongSubadditivity"
+holes = ["strong_subadditivity"]
+submitter = "Alex Meiburg"
+notes = "This fact is 'equivalent' to other facts such as the joint convexity of quantum relative entropy. First proved in 1973 by E.H. Lieb and M.B. Ruskai, but at least half-a-dozen alternate proofs have been published, with varied techniques. This formulation states the problem for all PSD matrices (over non-empty, finite index types) instead of restricting to normalized matrices of trace one. This is because `S(t·σ) = t·S(σ) − t·log t` (for any t including negatives and zero, actually, under Mathlib's conventions). Since all entropies are of matrices of the same trace, all can be rescaled to unit trace by the same t, and the constant shifts `−t·log t` cancel out."
+source = "E. H. Lieb and M. B. Ruskai, 'Proof of the strong subadditivity of quantum-mechanical entropy', J. Math. Phys. 14(12), 1938–1941 (1973), doi:10.1063/1.1666274."
+informal_solution = "First establish the joint convexity or quantum relative entropy, then the data processing inequality for quantum relative entropy (also known as monotonicity). Apply DPI to the relative entropy between states ρABC and the tensor product state ρAB ⊗ ρC, where the applied channel is partial tracing out the A subsystem. Then expanding out relative entropy in terms of logs and cancelling terms gives the desired inequality."