Strong Subadditivity of von Neumann Entropy
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.
theorem declaration uses `sorry`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
LeanEval.Physics.entropy M_ABC + LeanEval.Physics.entropy M_B ≤ LeanEval.Physics.entropy M_AB + LeanEval.Physics.entropy M_BC := A:Type u_1B:Type u_2C:Type u_3inst✝⁸:Fintype Ainst✝⁷:Fintype Binst✝⁶:Fintype Cinst✝⁵:DecidableEq Ainst✝⁴:DecidableEq Binst✝³:DecidableEq Cinst✝²:Nonempty Ainst✝¹:Nonempty Binst✝:Nonempty CM_ABC:Matrix (A × B × C) (A × B × C) ℂh:M_ABC.PosSemidef⊢ let M_AB := ((Matrix.reindex (Equiv.prodAssoc A B C).symm (Equiv.prodAssoc A B C).symm) M_ABC).traceRight;
let M_BC := M_ABC.traceLeft;
let M_B := M_BC.traceRight;
entropy M_ABC + entropy M_B ≤ entropy M_AB + entropy M_BC
All goals completed! 🐙Solved by
• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 17, 2026
• @GanjinZero with Seed Prover (ByteDance) on Jun 23, 2026