Frobenius inner product of PSD matrices is nonnegative

Proved

EthierKurtz.posSemidef_frobenius_nonneg

by caleb · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebramatrices

This is the linear-algebra fact that the Frobenius inner product of two positive-semidefinite matrices is nonnegative.

Let $d$ be a natural number and let $A, H$ be real $d \times d$ matrices, both positive-semidefinite. Then

\sum_{i,j} A_{ij} H_{ij} \ge 0.

Equivalently, the trace $\mathrm{tr}(AH)$ is nonnegative. The proof diagonalizes $A = U\Lambda U^*$ by the spectral theorem and rewrites the sum as $\sum_k \lambda_k\, u_k^* H u_k$ with $\lambda_k \ge 0$ and each quadratic form nonnegative. This isolates the entire spectral argument used when passing from Hessian positive-semidefiniteness to the sign of a second-order elliptic operator at a minimum point.

Formalization Note Positive-semidefiniteness is Mathlib's Matrix.PosSemidef; the proof uses spectral_theorem, eigenvalues_nonneg, and dotProduct_mulVec_nonneg.

Preamble

import Mathlib

open scoped Topology

Formal statement

namespace EthierKurtz

theorem posSemidef_frobenius_nonneg {d : ℕ}
    (A H : Matrix (Fin d) (Fin d) ℝ)
    (hA : A.PosSemidef) (hH : H.PosSemidef) :
    0 ≤ ∑ i, ∑ j, A i j * H i j := by sorry

end EthierKurtz

Source

Frobenius inner product / trace of a product of positive-semidefinite matrices is nonnegative, via the spectral theorem. https://en.wikipedia.org/wiki/Positive-semidefinite_matrix

View graph