On this page

Von Neumann's trace inequality and the Hoffman-Wielandt inequality

GaussianAnalysis.matrix.von_neumannlibrary/matrix/von_neumann.v395 lines21 lemmas and theorems, 2 definitionssource

Imports 2 library modules and 12 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.finite_group.fingroup, mathcomp.finite_group.perm, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.reals.reals, mathcomp.algebra.ring_tactic

Imported by 5

Required by 8 files of the paper proofs

For a real symmetric matrix A of size n, spec A is the row vector of its eigenvalues in decreasing order, obtained by sorting the diagonal of the spectral decomposition of real_spectral.v (sym_spectral_diag). This file is part of item G7 of phase 5 (the semicircle law, random_matrix/wigner.v): the Hoffman-Wielandt inequality makes the linear statistics of eigenvalues Lipschitz functions of the matrix, so that Gaussian concentration applies to them, and von Neumann's inequality is used in Lemma 5.14 of Koehler and Sohn (arXiv 2608.27372, line 5909).

Main results:

spec_decr, spec_perm, sum_spec, spec_decomposition: spec A is decreasing and is a permutation of sym_spectral_diag A, so \sum_i f (spec A 0 i) does not depend on the decomposition; A = P^T diag_mx (spec A) P for some orthogonal P when A is symmetric.
abel_ge0, abel_ge0_sum0: Abel summation, sum_i a_i w_i >= 0 for a decreasing (and nonnegative, or with sum_i w_i = 0) and w with nonnegative partial sums; sum_weight_le: for b decreasing and weights 0 <= c_j <= 1 of total k, sum_j b_j c_j is at most the sum of the k largest b_j.
doubly_stochastic_le, doubly_stochastic_le_mx: for a and b decreasing and M doubly stochastic, sum_(i, j) a_i b_j M_ij <= sum_i a_i b_i (without Birkhoff's theorem); orthogonal_sqr_row, orthogonal_sqr_col: the squared entries of an orthogonal matrix form a doubly stochastic matrix.
von_neumann_trace: \tr (A B) <= sum_i spec A 0 i * spec B 0 i for A and B symmetric.
mxdot_spec: |A|_F^2 = sum_i spec A 0 i ^+ 2; hoffman_wielandt: sum_i (spec A 0 i - spec B 0 i)^2 <= |A - B|_F^2 for A and B symmetric; spec_lipschitz: each eigenvalue is 1-Lipschitz for the Frobenius norm; spec_stat_lipschitz: for f L-Lipschitz, A |-> sum_i f (spec A 0 i) is (L sqrt n)-Lipschitz for the Frobenius norm on symmetric matrices.

`spec_seq A`	the sorted list of the eigenvalues of A
`spec A`	the eigenvalues of the symmetric matrix A, in decreasing order

Main results

Results	Statement
specspec_decrspec_permsum_specspec_decomposition	`spec A` is the row of the eigenvalues of a symmetric matrix `A` in decreasing order (the sorted diagonal of `sym_spectral_diag A`): `A = P^T diag_mx (spec A) P` for some orthogonal `P`, and `\sum_i f (spec A 0 i)` is the same sum over the diagonal of any spectral decomposition.
abel_ge0abel_ge0_sum0sum_weight_ledoubly_stochastic_ledoubly_stochastic_le_mxorthogonal_sqr_roworthogonal_sqr_col	Abel summation: `sum_i a_i w_i >= 0` for `a` decreasing and `w` with nonnegative partial sums, when `a >= 0` or `sum_i w_i = 0`. For `a` and `b` decreasing and `M` doubly stochastic, `sum_(i, j) a_i b_j M_ij <= sum_i a_i b_i`, without Birkhoff's theorem; the squared entries of an orthogonal matrix form a doubly stochastic matrix.
von_neumann_tracemxdot_spechoffman_wielandtspec_lipschitzspec_stat_lipschitz	Von Neumann's trace inequality `\tr (A B) <= sum_i spec A 0 i * spec B 0 i` and the Hoffman-Wielandt inequality `sum_i (spec A 0 i - spec B 0 i)^2 <= \|A - B\|_F^2` for `A`, `B` symmetric. So each eigenvalue is 1-Lipschitz for the Frobenius norm, and for `f` `L`-Lipschitz, `A \|-> sum_i f (spec A 0 i)` is `(L sqrt n)`-Lipschitz.

Declarations23 exported

sectionspec

Context {R : realType} {n : nat}.
Implicit Types A B : 'M[R]_n.

definition spec_seq source, line 62

Type

forall {R : realType} {n : nat}, 'M_n -> seq R

Definition

Definition spec_seq A : seq R :=
  sort (fun x y => y <= x) [seq sym_spectral_diag A 0 i | i <- enum 'I_n].

The eigenvalues of a symmetric matrix, sorted decreasingly.

Used by 7 declarations in 2 files

this file: spec, size_spec_seq, perm_spec_seq, sorted_spec_seq, spec_perm, von_neumann_trace
GaussianAnalysis.matrix.psd_part: spec_conj_diag

definition spec main result source, line 65

Type

forall {R : realType} {n : nat}, 'M_n -> 'rV_n

Definition

Definition spec A : 'rV[R]_n := \row_i nth 0 (spec_seq A) i.

Main result, as the README states it

spec A is the row of the eigenvalues of a symmetric matrix A in decreasing order (the sorted diagonal of sym_spectral_diag A): A = P^T diag_mx (spec A) P for some orthogonal P, and \sum_i f (spec A 0 i) is the same sum over the diagonal of any spectral decomposition.

Used by 37 declarations in 6 files

this file: spec_decr, spec_perm, sum_spec, spec_decomposition, sum_spec_exp, von_neumann_trace, mxdot_spec, hoffman_wielandt, spec_lipschitz, spec_stat_lipschitz
GaussianAnalysis.matrix.psd_part: spec_shift_decomposition, trace_psd_part_shift, frobenius_psd_part_shift, spec_conj_diag, spec_scale, spec_psd_ge0, sum_spec_trace, mxdot_spec_le, mxdot_psd_part_shift
GaussianAnalysis.matrix.effective_rank: effective_rank_spec
GaussianAnalysis.matrix.condition_cone: cond_coneP, cond_cone_quad, cond_energy, cond_energy_le, cond_energyZ, cond_energy_mono, cond_dist_itv, cond_slice_t, cond_slice_spec, cond_slice_frobenius, cond_cone_slice
GaussianAnalysis.random_matrix.goe: spec_le_opnorm, goe_clip, goe_trE
GaussianAnalysis.random_matrix.wigner: goe_stat, continuous_goe_stat, goe_stat_near

lemma size_spec_seq source, line 67

forall {R : realType} {n : nat} (A : 'M_n), size (spec_seq A) = n

Statement as written in the source

Lemma size_spec_seq A : size (spec_seq A) = n.

Used by 1 declaration in 1 file

this file: spec_decr

lemma perm_spec_seq source, line 70

forall {R : realType} {n : nat} (A : 'M_n),
perm_eq (spec_seq A) [seq sym_spectral_diag A 0 i | i <- enum 'I_n]

Statement as written in the source

Lemma perm_spec_seq A :
  perm_eq (spec_seq A) [seq sym_spectral_diag A 0 i | i <- enum 'I_n].

Used by 1 declaration in 1 file

this file: spec_perm

lemma sorted_spec_seq source, line 74

forall {R : realType} {n : nat} (A : 'M_n), sorted (fun x : R => <=%R^~ x) (spec_seq A)

Statement as written in the source

Lemma sorted_spec_seq A : sorted (fun x y : R => y <= x) (spec_seq A).

Used by 1 declaration in 1 file

this file: spec_decr

lemma spec_decr main result source, line 78

forall {R : realType} {n : nat} (A : 'M_n) [i j : 'I_n],
(i <= j)%N -> spec A 0 j <= spec A 0 i

The spectrum is decreasing.

Main result

Stated in the README together with spec.

Statement as written in the source

Lemma spec_decr A (i j : 'I_n) : (i <= j)%N -> spec A 0 j <= spec A 0 i.

Used by 4 declarations in 4 files

this file: von_neumann_trace
GaussianAnalysis.matrix.psd_part: spec_scale
GaussianAnalysis.matrix.effective_rank: effective_rank_spec
GaussianAnalysis.matrix.condition_cone: cond_cone_quad

lemma spec_perm main result source, line 89

forall {R : realType} {n : nat} (A : 'M_n),
exists s : {perm 'I_n}, forall i : 'I_n, spec A 0 i = sym_spectral_diag A 0 (s i)

The spectrum is a permutation of the diagonal of the chosen spectral decomposition.

Main result

Stated in the README together with spec.

Statement as written in the source

Lemma spec_perm A : exists s : 'S_n,
  forall i, spec A 0 i = sym_spectral_diag A 0 (s i).

Used by 2 declarations in 1 file

this file: sum_spec, spec_decomposition

lemma sum_spec main result source, line 99

forall {R : realType} {n : nat} (A : 'M_n) (f : R -> R),
\sum_i f (spec A 0 i) = \sum_i f (sym_spectral_diag A 0 i)

Sums over the spectrum.

Main result

Stated in the README together with spec.

Statement as written in the source

Lemma sum_spec A (f : R -> R) :
  \sum_i f (spec A 0 i) = \sum_i f (sym_spectral_diag A 0 i).

Used by 1 declaration in 1 file

GaussianAnalysis.matrix.condition_cone: cond_clip_energy

lemma spec_decomposition main result source, line 108

forall {R : realType} {n : nat} [A : 'M_n],
A \is symmetricmx ->
exists2 P : 'M_n, P \is orthogonalmx & A = P^T *m diag_mx (spec A) *m P

A = P^T diag (spec A) P for some orthogonal P.

Main result

Stated in the README together with spec.

Statement as written in the source

Lemma spec_decomposition A : A \is symmetricmx ->
  exists2 P : 'M[R]_n, P \is orthogonalmx & A = P^T *m diag_mx (spec A) *m P.

Used by 15 declarations in 5 files

this file: sum_spec_exp, von_neumann_trace, mxdot_spec
GaussianAnalysis.matrix.psd_part: spec_shift_decomposition, spec_scale, spec_psd_ge0, sum_spec_trace, mxdot_psd_part_shift
GaussianAnalysis.matrix.effective_rank: effective_rank_spec
GaussianAnalysis.matrix.condition_cone: cond_coneP, cond_cone_quad, cond_slice_t, cond_slice_form, cond_cone_slice
GaussianAnalysis.random_matrix.goe: spec_le_opnorm

sectionabel

Context {R : realFieldType}.

lemma decr_le source, line 132

forall {R : realFieldType} [n : nat] [a : nat -> R],
(forall i : nat, (i.+1 < n)%N -> a i.+1 <= a i) ->
forall [i j : nat], (i <= j)%N -> (j < n)%N -> a j <= a i

A sequence decreasing on [0, n) is decreasing between any two indices.

Statement as written in the source

Lemma decr_le n (a : nat -> R) : (forall i, (i.+1 < n)%N -> a i.+1 <= a i) ->
  forall i j, (i <= j)%N -> (j < n)%N -> a j <= a i.

Used by 2 declarations in 1 file

this file: abel_ge0, abel_ge0_sum0

lemma abel_ge0 main result source, line 142

forall {R : realFieldType} [n : nat] [a w : nat -> R],
(forall i : nat, (i.+1 < n)%N -> a i.+1 <= a i) ->
(forall i : nat, (i < n)%N -> 0 <= a i) ->
(forall k : nat, (k <= n)%N -> 0 <= \sum_(i < k) w i) -> 0 <= \sum_(i < n) a i * w i

Abel summation: if a is decreasing and nonnegative on [0, n) and the partial sums of w are nonnegative, then sum_(i < n) a i w i >= 0.

Main result, as the README states it

Abel summation: sum_i a_i w_i >= 0 for a decreasing and w with nonnegative partial sums, when a >= 0 or sum_i w_i = 0. For a and b decreasing and M doubly stochastic, sum_(i, j) a_i b_j M_ij <= sum_i a_i b_i, without Birkhoff's theorem; the squared entries of an orthogonal matrix form a doubly stochastic matrix.

Statement as written in the source

Lemma abel_ge0 n (a w : nat -> R) :
  (forall i, (i.+1 < n)%N -> a i.+1 <= a i) ->
  (forall i, (i < n)%N -> 0 <= a i) ->
  (forall k, (k <= n)%N -> 0 <= \sum_(i < k) w i) ->
  0 <= \sum_(i < n) a i * w i.

Used by 1 declaration in 1 file

this file: abel_ge0_sum0

lemma abel_ge0_sum0 main result source, line 162

forall {R : realFieldType} [n : nat] [a w : nat -> R],
(forall i : nat, (i.+1 < n)%N -> a i.+1 <= a i) ->
(forall k : nat, (k <= n)%N -> 0 <= \sum_(i < k) w i) ->
\sum_(i < n) w i = 0 -> 0 <= \sum_(i < n) a i * w i

The same with a of any sign, when the sum of w is 0.

Main result

Stated in the README together with abel_ge0.

Statement as written in the source

Lemma abel_ge0_sum0 n (a w : nat -> R) :
  (forall i, (i.+1 < n)%N -> a i.+1 <= a i) ->
  (forall k, (k <= n)%N -> 0 <= \sum_(i < k) w i) -> \sum_(i < n) w i = 0 ->
  0 <= \sum_(i < n) a i * w i.

Used by 2 declarations in 1 file

this file: sum_weight_le, doubly_stochastic_le

lemma sum_weight_le main result source, line 178

forall {R : realFieldType} [n k : nat] [b c : nat -> R],
(k <= n)%N ->
(forall i : nat, (i.+1 < n)%N -> b i.+1 <= b i) ->
(forall j : nat, (j < n)%N -> 0 <= c j <= 1) ->
\sum_(j < n) c j = k%:R -> \sum_(j < n) b j * c j <= \sum_(j < k) b j

For b decreasing and 0 <= c j <= 1 with sum_j c j = k, the sum of b j c j is at most the sum of the k largest b j.

Main result

Stated in the README together with abel_ge0.

Statement as written in the source

Lemma sum_weight_le n k (b c : nat -> R) : (k <= n)%N ->
  (forall i, (i.+1 < n)%N -> b i.+1 <= b i) ->
  (forall j, (j < n)%N -> 0 <= c j <= 1) -> \sum_(j < n) c j = k%:R ->
  \sum_(j < n) b j * c j <= \sum_(j < k) b j.

Used by 1 declaration in 1 file

this file: doubly_stochastic_le

lemma doubly_stochastic_le main result source, line 209

forall {R : realFieldType} [n : nat] [a b : nat -> R] [M : 'M_n],
(forall i : nat, (i.+1 < n)%N -> a i.+1 <= a i) ->
(forall i : nat, (i.+1 < n)%N -> b i.+1 <= b i) ->
(forall i j : 'I_n, 0 <= M i j) ->
(forall i : 'I_n, \sum_j M i j = 1) ->
(forall j : 'I_n, \sum_i M i j = 1) ->
\sum_(i < n) \sum_(j < n) a i * b j * M i j <= \sum_(i < n) a i * b i

For a and b decreasing and M doubly stochastic, sum_(i, j) a i b j M i j <= sum_i a i b i.

Main result

Stated in the README together with abel_ge0.

Statement as written in the source

Lemma doubly_stochastic_le n (a b : nat -> R) (M : 'M[R]_n) :
  (forall i, (i.+1 < n)%N -> a i.+1 <= a i) ->
  (forall i, (i.+1 < n)%N -> b i.+1 <= b i) ->
  (forall i j, 0 <= M i j) -> (forall i, \sum_j M i j = 1) ->
  (forall j, \sum_i M i j = 1) ->
  \sum_(i < n) \sum_(j < n) a i * b j * M i j <= \sum_(i < n) a i * b i.

Used by 1 declaration in 1 file

this file: doubly_stochastic_le_mx

lemma doubly_stochastic_le_mx main result source, line 250

forall {R : realFieldType} [n : nat] [a b : 'rV_n] [M : 'M_n],
(forall i j : 'I_n, (i <= j)%N -> a 0 j <= a 0 i) ->
(forall i j : 'I_n, (i <= j)%N -> b 0 j <= b 0 i) ->
(forall i j : 'I_n, 0 <= M i j) ->
(forall i : 'I_n, \sum_j M i j = 1) ->
(forall j : 'I_n, \sum_i M i j = 1) ->
\sum_i \sum_j a 0 i * b 0 j * M i j <= \sum_i a 0 i * b 0 i

The same for row vectors a and b, decreasing in the order of 'I_n.

Main result

Stated in the README together with abel_ge0.

Statement as written in the source

Lemma doubly_stochastic_le_mx n (a b : 'rV[R]_n) (M : 'M[R]_n) :
  (forall i j : 'I_n, (i <= j)%N -> a 0 j <= a 0 i) ->
  (forall i j : 'I_n, (i <= j)%N -> b 0 j <= b 0 i) ->
  (forall i j, 0 <= M i j) -> (forall i, \sum_j M i j = 1) ->
  (forall j, \sum_i M i j = 1) ->
  \sum_i \sum_j a 0 i * b 0 j * M i j <= \sum_i a 0 i * b 0 i.

Used by 1 declaration in 1 file

this file: von_neumann_trace

sectionvon_neumann

Context {R : realType} {n : nat}.
Implicit Types A B : 'M[R]_n.

lemma orthogonal_sqr_row main result source, line 276

forall {R : realType} {n : nat} [U : 'M_n] (i : 'I_n),
U \is orthogonalmx -> \sum_j U i j ^+ 2 = 1

The squared entries of an orthogonal matrix form a doubly stochastic matrix.

Main result

Stated in the README together with abel_ge0.

Statement as written in the source

Lemma orthogonal_sqr_row (U : 'M[R]_n) i : U \is orthogonalmx ->
  \sum_j U i j ^+ 2 = 1.

Used by 2 declarations in 1 file

this file: orthogonal_sqr_col, von_neumann_trace

lemma orthogonal_sqr_col main result source, line 284

forall {R : realType} {n : nat} [U : 'M_n] (j : 'I_n),
U \is orthogonalmx -> \sum_i U i j ^+ 2 = 1

Main result

Stated in the README together with abel_ge0.

Statement as written in the source

Lemma orthogonal_sqr_col (U : 'M[R]_n) j : U \is orthogonalmx ->
  \sum_i U i j ^+ 2 = 1.

Used by 1 declaration in 1 file

this file: von_neumann_trace

lemma sum_spec_exp source, line 292

forall {R : realType} {n : nat} [A : 'M_n] (k : nat),
A \is symmetricmx -> \sum_i spec A 0 i ^+ k = \tr (A ^+ k)

The power sums of the spectrum are the traces of the powers.

Statement as written in the source

Lemma sum_spec_exp A k : A \is symmetricmx ->
  \sum_i spec A 0 i ^+ k = \tr (A ^+ k).

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.goe: goe_trE

theorem von_neumann_trace main result source, line 301

forall {R : realType} {n : nat} [A B : 'M_n],
A \is symmetricmx -> B \is symmetricmx -> \tr (A *m B) <= \sum_i spec A 0 i * spec B 0 i

von Neumann's trace inequality.

Main result, as the README states it

Von Neumann's trace inequality \tr (A B) <= sum_i spec A 0 i * spec B 0 i and the Hoffman-Wielandt inequality sum_i (spec A 0 i - spec B 0 i)^2 <= |A - B|_F^2 for A, B symmetric. So each eigenvalue is 1-Lipschitz for the Frobenius norm, and for f L-Lipschitz, A |-> sum_i f (spec A 0 i) is (L sqrt n)-Lipschitz.

Statement as written in the source

Theorem von_neumann_trace A B : A \is symmetricmx -> B \is symmetricmx ->
  \tr (A *m B) <= \sum_i spec A 0 i * spec B 0 i.

Used by 2 declarations in 2 files

this file: hoffman_wielandt
GaussianAnalysis.matrix.psd_part: mxdot_spec_le

lemma mxdot_spec main result source, line 329

forall {R : realType} {n : nat} [A : 'M_n],
A \is symmetricmx -> mxdot A A = \sum_i spec A 0 i ^+ 2

The Frobenius norm is the Euclidean norm of the spectrum.

Main result

Stated in the README together with von_neumann_trace.

Statement as written in the source

Lemma mxdot_spec A : A \is symmetricmx -> mxdot A A = \sum_i spec A 0 i ^+ 2.

Used by 2 declarations in 2 files

this file: hoffman_wielandt
GaussianAnalysis.matrix.condition_cone: cond_slice_frobenius

theorem hoffman_wielandt main result source, line 336

forall {R : realType} {n : nat} [A B : 'M_n],
A \is symmetricmx ->
B \is symmetricmx -> \sum_i (spec A 0 i - spec B 0 i) ^+ 2 <= mxdot (A - B) (A - B)

The Hoffman-Wielandt inequality.

Main result

Stated in the README together with von_neumann_trace.

Statement as written in the source

Theorem hoffman_wielandt A B : A \is symmetricmx -> B \is symmetricmx ->
  \sum_i (spec A 0 i - spec B 0 i) ^+ 2 <= mxdot (A - B) (A - B).

Used by 3 declarations in 2 files

this file: spec_lipschitz, spec_stat_lipschitz
GaussianAnalysis.matrix.condition_cone: cond_energy_le

lemma spec_lipschitz main result source, line 354

forall {R : realType} {n : nat} [A B : 'M_n] (i : 'I_n),
A \is symmetricmx -> B \is symmetricmx -> `|spec A 0 i - spec B 0 i| <= frobenius (A - B)

The sorted spectrum is 1-Lipschitz for the Frobenius norm.

Main result

Stated in the README together with von_neumann_trace.

Statement as written in the source

Lemma spec_lipschitz A B (i : 'I_n) : A \is symmetricmx -> B \is symmetricmx ->
  `|spec A 0 i - spec B 0 i| <= frobenius (A - B).

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.wigner: continuous_goe_stat

lemma spec_stat_lipschitz main result source, line 366

forall {R : realType} {n : nat} [f : R -> R] [L : R] [A B : 'M_n],
A \is symmetricmx ->
B \is symmetricmx ->
(forall x y : R, `|f x - f y| <= L * `|x - y|) ->
`|\sum_i f (spec A 0 i) - \sum_i f (spec B 0 i)| <=
L * Num.ExtraDef.sqrtr n%:R * frobenius (A - B)

A linear statistic of the spectrum of an L-Lipschitz function is (L sqrt n)-Lipschitz for the Frobenius norm.

Main result

Stated in the README together with von_neumann_trace.

Statement as written in the source

Lemma spec_stat_lipschitz (f : R -> R) (L : R) A B :
  A \is symmetricmx -> B \is symmetricmx ->
  (forall x y, `|f x - f y| <= L * `|x - y|) ->
  `|\sum_i f (spec A 0 i) - \sum_i f (spec B 0 i)| <=
    L * Num.sqrt n%:R * frobenius (A - B).

Used by 2 declarations in 2 files

GaussianAnalysis.random_matrix.goe: goe_clip_lipschitz
GaussianAnalysis.random_matrix.wigner: goe_stat_lipschitz

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.