Strong Subadditivity of von Neumann Entropy

strong_subadditivity — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- 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. -/
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

Informal solution sketch

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.

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.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: strong_subadditivity
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Alex Meiburg.