From f791e353f9931714841824b2bef5448334a9a682 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Fri, 29 May 2026 12:44:51 -0400 Subject: [PATCH 1/6] Create StrongSubadditivity.lean --- LeanEval/Physics/StrongSubadditivity.lean | 45 +++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 LeanEval/Physics/StrongSubadditivity.lean diff --git a/LeanEval/Physics/StrongSubadditivity.lean b/LeanEval/Physics/StrongSubadditivity.lean new file mode 100644 index 0000000..5424543 --- /dev/null +++ b/LeanEval/Physics/StrongSubadditivity.lean @@ -0,0 +1,45 @@ +import EvalTools.Markers +import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus +import Mathlib.LinearAlgebra.Matrix.PosDef + +/-! # Strong additivity of quantum entropy + +States that `S(ρ_ABC) + S(ρ_B) ≤ S(ρ_AB) + S(ρ_C)` where S is the von Neumman entropy. + +[Wikipedia article](https://en.wikipedia.org/wiki/Strong_subadditivity_of_quantum_entropy) on +the significance of this inequality. + +-/ + +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 Matrix.traceLeft (M : Matrix (A × B) (A × B) ℂ) : Matrix B B ℂ := + Matrix.of fun i j ↦ ∑ k, ∑ l, M (k, i) (l, j) + +/-- Partial trace on the right of a matrix -/ +def Matrix.traceRight (M : Matrix (A × B) (A × B) ℂ) : Matrix A A ℂ := + Matrix.of fun i j ↦ ∑ k, ∑ l, M (i, k) (j, l) + +/-- 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 StrongSubadditivity (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 From 61e0449860990d199ed1c6e7e73e75a2f3818fc7 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Fri, 29 May 2026 12:47:40 -0400 Subject: [PATCH 2/6] Update StrongSubadditivity.lean --- LeanEval/Physics/StrongSubadditivity.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/LeanEval/Physics/StrongSubadditivity.lean b/LeanEval/Physics/StrongSubadditivity.lean index 5424543..f3a9b44 100644 --- a/LeanEval/Physics/StrongSubadditivity.lean +++ b/LeanEval/Physics/StrongSubadditivity.lean @@ -11,6 +11,9 @@ 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] @@ -36,10 +39,13 @@ open ComplexOrder 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 StrongSubadditivity (M_ABC : Matrix (A × B × C) (A × B × C) ℂ) (h : M_ABC.PosSemidef) : +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 Physics +end LeanEval From 8d832606e7603aeb567105efbff0739c442600d8 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Fri, 29 May 2026 12:50:31 -0400 Subject: [PATCH 3/6] Create strong_subadditivity.toml --- manifests/problems/strong_subadditivity.toml | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 manifests/problems/strong_subadditivity.toml diff --git a/manifests/problems/strong_subadditivity.toml b/manifests/problems/strong_subadditivity.toml new file mode 100644 index 0000000..61668ff --- /dev/null +++ b/manifests/problems/strong_subadditivity.toml @@ -0,0 +1,7 @@ +id = "strong_subadditivity" +title = "Strong Subadditivity of von Neumann Entropy" +test = false +module = "LeanEval.Physics" +holes = ["strong_subadditivity"] +submitter = "Alex Meiburg" +notes = "This fact is 'equivalent' to other facts such as the joint convexity of quantum relative entropy. This formulation states the problem for all PSD matrices (over non-empty, finite index types) instead of unnecessarily restricting to normalized matrices of trace one. 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." From 8cd3ba5223d98a3c2d0627c4332bcfd5bf134245 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Mon, 8 Jun 2026 12:12:37 -0400 Subject: [PATCH 4/6] Update StrongSubadditivity.lean --- LeanEval/Physics/StrongSubadditivity.lean | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/LeanEval/Physics/StrongSubadditivity.lean b/LeanEval/Physics/StrongSubadditivity.lean index f3a9b44..6026b9e 100644 --- a/LeanEval/Physics/StrongSubadditivity.lean +++ b/LeanEval/Physics/StrongSubadditivity.lean @@ -1,10 +1,10 @@ -import EvalTools.Markers +-- import EvalTools.Markers import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus import Mathlib.LinearAlgebra.Matrix.PosDef -/-! # Strong additivity of quantum entropy +/-! # Strong subadditivity of quantum entropy -States that `S(ρ_ABC) + S(ρ_B) ≤ S(ρ_AB) + S(ρ_C)` where S is the von Neumman 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. @@ -22,12 +22,12 @@ variable [Nonempty A] [Nonempty B] [Nonempty C] noncomputable section /-- Partial trace on the left of a matrix -/ -def Matrix.traceLeft (M : Matrix (A × B) (A × B) ℂ) : Matrix B B ℂ := - Matrix.of fun i j ↦ ∑ k, ∑ l, M (k, i) (l, j) +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 Matrix.traceRight (M : Matrix (A × B) (A × B) ℂ) : Matrix A A ℂ := - Matrix.of fun i j ↦ ∑ k, ∑ l, M (i, k) (j, l) +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 ℂ) : ℝ := @@ -47,5 +47,7 @@ theorem strong_subadditivity (M_ABC : Matrix (A × B × C) (A × B × C) ℂ) (h entropy M_ABC + entropy M_B ≤ entropy M_AB + entropy M_BC := by sorry +end + end Physics end LeanEval From 197b3414a14233319380c030520c8e781d0f8424 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Mon, 8 Jun 2026 12:24:40 -0400 Subject: [PATCH 5/6] Update strong_subadditivity.toml --- manifests/problems/strong_subadditivity.toml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/manifests/problems/strong_subadditivity.toml b/manifests/problems/strong_subadditivity.toml index 61668ff..6c609b6 100644 --- a/manifests/problems/strong_subadditivity.toml +++ b/manifests/problems/strong_subadditivity.toml @@ -1,7 +1,9 @@ id = "strong_subadditivity" title = "Strong Subadditivity of von Neumann Entropy" test = false -module = "LeanEval.Physics" +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. This formulation states the problem for all PSD matrices (over non-empty, finite index types) instead of unnecessarily restricting to normalized matrices of trace one. 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." +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." From f4af9969beb18bb9cc36d6c5f46c195467c7c7a8 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Mon, 8 Jun 2026 12:25:21 -0400 Subject: [PATCH 6/6] oop --- LeanEval/Physics/StrongSubadditivity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanEval/Physics/StrongSubadditivity.lean b/LeanEval/Physics/StrongSubadditivity.lean index 6026b9e..0b47bc1 100644 --- a/LeanEval/Physics/StrongSubadditivity.lean +++ b/LeanEval/Physics/StrongSubadditivity.lean @@ -1,4 +1,4 @@ --- import EvalTools.Markers +import EvalTools.Markers import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus import Mathlib.LinearAlgebra.Matrix.PosDef