Jensen's operator inequality for isometries

Let V be an isometry, a rectangular matrix with Vᴴ * V = 1, and let f be operator concave: A ↦ cfc f A is concave on a set S of square matrices closed under unitary conjugation. Then compressing by V lowers the functional calculus,

Vᴴ * cfc f A * V ≤ cfc f (Vᴴ * A * V) for Hermitian A ∈ S,

Matrix.conjTranspose_mul_cfc_mul_le_cfc_conjTranspose_mul_mul. For the logarithm, which Mathlib proves operator concave on the strictly positive elements (CFC.concaveOn_log), this is the compression inequality -log (Vᴴ * A * V) ≤ Vᴴ * (-log A) * V for positive definite A, Matrix.PosDef.conjTranspose_mul_log_mul_le_log. Applied to the partial-trace isometry and the relative modular operator, this compression inequality is the operator inequality behind the monotonicity of the relative entropy under partial traces, and so behind the strong subadditivity of the von Neumann entropy.

The argument

Let P = V * Vᴴ be the projection onto the range of V and U = 2 • P - 1 the reflection across it, a self-adjoint unitary with U * V = V. The pinching C = (A + U * A * U) / 2 of A is P * A * P + (1 - P) * A * (1 - P), so the range of V is invariant, C * V = V * (Vᴴ * A * V). The functional calculus preserves intertwiners (Matrix.IsHermitian.cfc_mul_eq_mul_cfc), hence Vᴴ * cfc f C * V = cfc f (Vᴴ * A * V) and cfc f (U * A * U) = U * cfc f A * U. Concavity at the midpoint gives (cfc f A + U * cfc f A * U) / 2 ≤ cfc f C, and compressing both sides by V gives the inequality, since U * V = V.

References

• F. Hansen, G. K. Pedersen, Jensen's inequality for operators and Löwner's theorem, Math. Ann. 258 (1982), 229–241.
• F. Hansen, G. K. Pedersen, Jensen's operator inequality, Bull. London Math. Soc. 35 (2003), 553–564.
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer (1997), Section V.2 (operator convex functions and Jensen's inequality for compressions).

theorem Matrix.conjTranspose_mul_cfc_mul_le_cfc_conjTranspose_mul_mul {m : Type u_1} {n : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {f : ℝ → ℝ} {S : Set (Matrix m m 𝕜)} (hf : ConcaveOn ℝ S (cfc f)) (hS : ∀ a ∈ S, ∀ u ∈ unitary (Matrix m m 𝕜), u * a * star u ∈ S) {A : Matrix m m 𝕜} (hAS : A ∈ S) (hA : A.IsHermitian) {V : Matrix m n 𝕜} (hV : V.conjTranspose * V = 1) : V.conjTranspose * cfc f A * V ≤ cfc f (V.conjTranspose * A * V)

Jensen's operator inequality for isometries. Let f be operator concave on a set S of matrices closed under unitary conjugation, in the sense that A ↦ cfc f A is concave on S. For a Hermitian A ∈ S and an isometry V, that is Vᴴ * V = 1, compressing by V lowers the functional calculus: Vᴴ * cfc f A * V ≤ cfc f (Vᴴ * A * V).

theorem Matrix.PosDef.conjTranspose_mul_log_mul_le_log {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {A : Matrix m m ℂ} (hA : A.PosDef) {V : Matrix m n ℂ} (hV : V.conjTranspose * V = 1) : V.conjTranspose * CFC.log A * V ≤ CFC.log (V.conjTranspose * A * V)

The compression inequality for the logarithm. For a positive definite complex matrix A and an isometry V, that is Vᴴ * V = 1, Vᴴ * log A * V ≤ log (Vᴴ * A * V); equivalently, -log (Vᴴ * A * V) ≤ Vᴴ * (-log A) * V.