Von Neumann's trace inequality

TheoremThe quadratic form of a symmetric matrix in an orthonormal eigenbasis#✓fully proved

Let \(B\) be a real symmetric matrix with rows and columns indexed by a finite set \(I\), and let \((v_j)_{j \in I}\) be the orthonormal basis of \(\mathbb{R}^I\) of eigenvectors of \(B\) chosen by the spectral theorem, with \(B v_j = \beta_j v_j\). Then for every \(x \in \mathbb{R}^I\), \(\langle x, Bx \rangle = \sum_j \beta_j \langle v_j, x \rangle^2\).

theorem inner_toEuclideanLin_self_eq_sum {B : Matrix n n ℝ} (hB : B.IsHermitian)
    (x : EuclideanSpace ℝ n) :
    ⟪x, toEuclideanLin B x⟫ = ∑ j, hB.eigenvalues j * ⟪hB.eigenvectorBasis j, x⟫ ^ 2

Used by 1

Used byThe trace of a product of symmetric matrices in their eigenbases

TheoremThe trace of a product of symmetric matrices in their eigenbases#✓fully proved

Let \(A\) and \(B\) be real symmetric matrices with rows and columns indexed by a finite set \(I\). Let \((u_i)_{i \in I}\) and \((v_j)_{j \in I}\) be the orthonormal bases of \(\mathbb{R}^I\) of eigenvectors of \(A\) and \(B\) chosen by the spectral theorem, with \(A u_i = \alpha_i u_i\) and \(B v_j = \beta_j v_j\). Then \(\operatorname{tr}(AB) = \sum_i \sum_j \alpha_i \beta_j \langle v_j, u_i \rangle^2\).

theorem trace_mul_eq_sum_eigenvalues {A B : Matrix n n ℝ} (hA : A.IsHermitian)
    (hB : B.IsHermitian) :
    (A * B).trace = ∑ i, ∑ j, hA.eigenvalues i * hB.eigenvalues j *
      ⟪hB.eigenvectorBasis j, hA.eigenvectorBasis i⟫ ^ 2

Uses 1 · Used by 2

Proof usesThe quadratic form of a symmetric matrix in an orthonormal eigenbasis

Used byA pairing of eigenvalues bounds the trace of a product from below · A pairing of eigenvalues bounds the trace of a product from above

TheoremThe overlap matrix of two orthonormal bases is doubly stochastic#✓fully proved

Let \(I\) be a finite set and let \((u_i)_{i \in I}\) and \((v_j)_{j \in I}\) be orthonormal bases of \(\mathbb{R}^I\) with its standard inner product. Then the \(I \times I\) matrix with entries \(P_{ij} = \langle v_j, u_i \rangle^2\) is doubly stochastic: its entries are nonnegative and each of its rows and columns sums to \(1\).

theorem overlap_mem_doublyStochastic (u v : OrthonormalBasis n ℝ (EuclideanSpace ℝ n)) :
    (Matrix.of fun i j => ⟪v j, u i⟫ ^ 2) ∈ doublyStochastic ℝ n

Used by 2

Used byA pairing of eigenvalues bounds the trace of a product from below · A pairing of eigenvalues bounds the trace of a product from above

TheoremLinear functionals on doubly stochastic matrices are bounded below at a permutation#✓fully proved

Let \(I\) be a finite set, let \(P\) be a doubly stochastic real \(I \times I\) matrix (its entries are nonnegative and each of its rows and columns sums to \(1\)), and let \(c_{ij} \in \mathbb{R}\) for \(i, j \in I\). Then there is a permutation \(\sigma\) of \(I\) with \(\sum_i c_{i \sigma(i)} \le \sum_i \sum_j c_{ij} P_{ij}\). That is, the linear functional \(M \mapsto \sum_{i, j} c_{ij} M_{ij}\) takes a value at some permutation matrix that is at most its value at \(P\).

The proof uses Birkhoff's theorem.

theorem exists_perm_sum_le_of_mem_doublyStochastic {P : Matrix n n ℝ}
    (hP : P ∈ doublyStochastic ℝ n) (c : n → n → ℝ) :
    ∃ σ : Equiv.Perm n, ∑ i, c i (σ i) ≤ ∑ i, ∑ j, c i j * P i j

Used by 2

Used byA pairing of eigenvalues bounds the trace of a product from below · A pairing of eigenvalues bounds the trace of a product from above

TheoremA pairing of eigenvalues bounds the trace of a product from below#✓fully proved

Let \(A\) and \(B\) be real symmetric matrices with rows and columns indexed by a finite set \(I\), and let \((\alpha_i)_{i \in I}\) and \((\beta_i)_{i \in I}\) be their eigenvalues, listed with multiplicity. Then there is a permutation \(\sigma\) of \(I\) with \(\sum_i \alpha_i \beta_{\sigma(i)} \le \operatorname{tr}(AB)\).

This is the lower half of von Neumann's trace inequality, in pairing form.

theorem exists_perm_sum_mul_eigenvalues_le_trace_mul {A B : Matrix n n ℝ} (hA : A.IsHermitian)
    (hB : B.IsHermitian) :
    ∃ σ : Equiv.Perm n, ∑ i, hA.eigenvalues i * hB.eigenvalues (σ i) ≤ (A * B).trace

Uses 3

Proof usesLinear functionals on doubly stochastic matrices are bounded below at a permutation · The overlap matrix of two orthonormal bases is doubly stochastic · The trace of a product of symmetric matrices in their eigenbases

TheoremA pairing of eigenvalues bounds the trace of a product from above#✓fully proved

Let \(A\) and \(B\) be real symmetric matrices with rows and columns indexed by a finite set \(I\), and let \((\alpha_i)_{i \in I}\) and \((\beta_i)_{i \in I}\) be their eigenvalues, listed with multiplicity. Then there is a permutation \(\sigma\) of \(I\) with \(\operatorname{tr}(AB) \le \sum_i \alpha_i \beta_{\sigma(i)}\).

This is the upper half of von Neumann's trace inequality, in pairing form.

theorem exists_perm_trace_mul_le_sum_mul_eigenvalues {A B : Matrix n n ℝ} (hA : A.IsHermitian)
    (hB : B.IsHermitian) :
    ∃ σ : Equiv.Perm n, (A * B).trace ≤ ∑ i, hA.eigenvalues i * hB.eigenvalues (σ i)

Uses 3

Proof usesLinear functionals on doubly stochastic matrices are bounded below at a permutation · The overlap matrix of two orthonormal bases is doubly stochastic · The trace of a product of symmetric matrices in their eigenbases

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.