feat: add strong_subadditivity problem#348
Conversation
| /-- 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) |
There was a problem hiding this comment.
The "two copies of B" can be distinct here. Perhaps worth doing for future proofing.
| id = "strong_subadditivity" | ||
| title = "Strong Subadditivity of von Neumann Entropy" | ||
| test = false | ||
| module = "LeanEval.Physics" |
There was a problem hiding this comment.
Failing CI: the module field should be the full module path of the file, not the directory namespace. The build tries to compile LeanEval/Physics.lean, which doesn't exist (error: no such file or directory … LeanEval/Physics.lean). Should be:
module = "LeanEval.Physics.StrongSubadditivity"(cf. LeanEval.Geometry.LiouvilleArnold ↔ LeanEval/Geometry/LiouvilleArnold.lean.)
|
|
||
| /-! # Strong additivity of quantum entropy | ||
|
|
||
| States that `S(ρ_ABC) + S(ρ_B) ≤ S(ρ_AB) + S(ρ_C)` where S is the von Neumman entropy. |
There was a problem hiding this comment.
The docstring has the wrong reduced state on the RHS: it says S(ρ_C), but SSA here is
S(ρ_ABC) + S(ρ_B) ≤ S(ρ_AB) + S(ρ_BC)
matching the theorem body's M_BC.
| 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." |
There was a problem hiding this comment.
Small correction to the reasoning in notes: relaxing to PSD is valid, but not because "normalization just produces a positive affine transformation on the entropy." S(t·σ) = t·S(σ) − t·log t is affine in S(σ) only for a fixed t, and can't be applied per-term independently unless the same trace t is shared by every term. That's exactly what holds here: a genuine (trace-preserving) partial trace gives all four reduced states the common trace t, so with two entropy terms on each side the −t·log t corrections cancel and you recover normalized SSA scaled by t ≥ 0 (and t = 0 ⇒ ρ = 0, trivial). Worth rewording so a solver isn't pointed at the wrong argument — and note this depends on the partial traces being trace-preserving.
| import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus | ||
| import Mathlib.LinearAlgebra.Matrix.PosDef | ||
|
|
||
| /-! # Strong additivity of quantum entropy |
There was a problem hiding this comment.
Typo in the header: "Strong additivity" → "Strong subadditivity".
|
|
||
| /-! # Strong additivity of quantum entropy | ||
|
|
||
| States that `S(ρ_ABC) + S(ρ_B) ≤ S(ρ_AB) + S(ρ_C)` where S is the von Neumman entropy. |
There was a problem hiding this comment.
"von Neumman" → "von Neumann".
| 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." |
There was a problem hiding this comment.
Optional, for consistency with the other problems: consider adding a source field and an informal_solution sketch. Both are optional in the parser so CI won't complain without them, but most manifests carry them. Suggested 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.
2 participants
This PR adds the problem of strong subadditivity of von Neumann entropy for quantum states.