On this page

The positive part of a symmetric matrix

GaussianAnalysis.matrix.psd_partlibrary/matrix/psd_part.v430 lines20 lemmas and theorems, 3 definitionssource

Imports 3 library modules and 15 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.poly, mathcomp.algebra.polydiv, mathcomp.algebra.mxpoly, mathcomp.algebra.sesquilinear, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.reals.reals, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 6

Required by 5 files of the paper proofs

For a real symmetric matrix A with a spectral decomposition A = P^T diag(d) P, P orthogonal, the positive part psd_part A = P^T diag((d_i)_+) P is the nearest positive semidefinite matrix to A in the Frobenius norm. It is defined from the decomposition chosen by sym_spectralmx and sym_spectral_diag of real_spectral.v, and does not depend on that choice (psd_partE).

G8 (Koehler and Sohn, Lemma 5.14 and Proposition 5.15) handles spectral functions through psd_part, which is equivariant under orthogonal conjugation: Lemma 5.13 (random_matrix/goe_rotation.v) can be stated for any F with F (Q W Q^T) = Q F(W) Q^T for every orthogonal Q, such as W |-> psd_part (W - w(W) I) for a w(W) that depends only on the spectrum.

psd_conj: P^T diag(d) P >= 0 for d >= 0; mxdot_psd_ge0: <S, T> >= 0 for S, T >= 0.
psd_nearest: for A = P^T diag(d) P and S >= 0, |A - S|^2 >= |A - A_+|^2 + |A_+ - S|^2; psd_part_nearest, psd_part A is the nearest positive semidefinite matrix; psd_partE, psd_part A = P^T diag((d_i)_+) P for every spectral decomposition; psd_part_psd.
psd_part_conj: psd_part (Q A Q^T) = Q (psd_part A) Q^T, Q orthogonal.
psd_part_moreau: A = psd_part A - psd_part (- A) with <psd_part A, psd_part (- A)> = 0.
psd_part_nonexpansive: |psd_part A - psd_part B|_F <= |A - B|_F; psd_partZ: psd_part (c A) = c psd_part A for c >= 0.
spec_shift_decomposition, trace_psd_part_shift and frobenius_psd_part_shift: tr psd_part (A - w I) = sum_i (spec A i - w)_+ and |psd_part (A - w I)|_F^2 = sum_i (spec A i - w)_+^2, with spec of matrix/von_neumann.v; mxdot_psd_part_shift: <A, psd_part (A - w I)> = sum_i spec A i (spec A i - w)_+.
char_poly_conj_diag, spec_conj_diag: P^T diag(v) P has the characteristic polynomial prod_i (X - v_i), so its sorted spectrum is v when v is decreasing; spec_scale: spec (c A) = c spec A for c >= 0.
spec_psd_ge0, sum_spec_trace: the eigenvalues of a positive semidefinite matrix are nonnegative; they sum to the trace.
mxdot_spec_le: von Neumann's inequality for the Frobenius pairing, <A, B> <= sum_i spec A i spec B i for A and B symmetric.

`psdmx A`	A is symmetric with x^T A x >= 0 for every x
`pos_row d`	the row of the (d_i)_+
`psd_part A`	the positive part of A

Main results

Results	Statement
psd_partpsd_part_nearestpsd_partEpsd_part_conjpsd_part_moreaupsd_part_nonexpansivepsd_partZ	The positive part `P^T diag((d_i)_+) P` of a symmetric `A = P^T diag(d) P` is the nearest positive semidefinite matrix to `A` in the Frobenius norm, so it does not depend on the decomposition; it commutes with orthogonal conjugation, `A = A_+ - (-A)_+` with `<A_+, (-A)_+> = 0`, `A \|-> A_+` is 1-Lipschitz, and `(c A)_+ = c A_+` for `c >= 0`. `<S, T> >= 0` for `S, T >= 0` (`mxdot_psd_ge0`).
trace_psd_part_shiftfrobenius_psd_part_shiftmxdot_psd_part_shift	`tr (A - w I)_+ = sum_i (spec A i - w)_+`, `\|(A - w I)_+\|_F^2 = sum_i (spec A i - w)_+^2` and `<A, (A - w I)_+> = sum_i spec A i (spec A i - w)_+`, with the sorted eigenvalues `spec` of `matrix/von_neumann.v`.
char_poly_conj_diagspec_conj_diagspec_scalespec_psd_ge0sum_spec_tracemxdot_spec_le	For `P` orthogonal, `P^T diag(v) P` has the characteristic polynomial `prod_i (X - v_i)`, so its sorted spectrum is `v` when `v` is decreasing, and `spec (c A) = c spec A` for `c >= 0`. The eigenvalues of a positive semidefinite matrix are nonnegative and sum to the trace; von Neumann's inequality in the form `<A, B> <= sum_i spec A i spec B i` for `A`, `B` symmetric.

Declarations23 exported

sectionpsd_part

Variable R : realType.
Implicit Types n : nat.

definition psdmx source, line 69

Type

forall [R : realType] [n : nat], 'M_n -> Prop

Definition

Definition psdmx n (A : 'M[R]_n) : Prop :=
  A \is symmetricmx /\ forall x : 'cV[R]_n, 0 <= mxdot x (A *m x).

A >= 0: symmetric with nonnegative quadratic forms.

Used by 23 declarations in 4 files

GaussianAnalysis.matrix.psd_splitting: psdmx_conj, psdmxD, psdmx0, psdmx_sum, mxtrace_psd_ge0, spectral_nonneg_proj, two_matrix_split, frobenius_sum_psd_le, trace_quad_ge0, trace_quad_sub_le, psd_splitting_rel, psd_splitting
this file: psd_conj, mxdot_psd_ge0, psd_nearest, psd_partE, psd_part_psd, psd_part_nearest, psd_part_nonexpansive, spec_psd_ge0
GaussianAnalysis.random_matrix.matrix_series: mxtrace_mul_psd_le, psdmx_exp_even
GaussianApplications.PsdSplittingStatement: psd_splitting_statement

definition pos_row source, line 72

Type

forall [R : realType] [n : nat], 'rV_n -> 'rV_n

Definition

Definition pos_row n (d : 'rV[R]_n) : 'rV[R]_n := \row_i Num.max (d 0 i) 0.

Used by 5 declarations in 1 file

this file: psd_part, psd_nearest, psd_partE, psd_part_moreau, psd_partZ

definition psd_part main result source, line 74

Type

forall [R : realType] [n : nat], 'M_n -> 'M_n

Definition

Definition psd_part n (A : 'M[R]_n) : 'M[R]_n :=
  (sym_spectralmx A)^T *m diag_mx (pos_row (sym_spectral_diag A)) *m
  sym_spectralmx A.

Main result, as the README states it

The positive part P^T diag((d_i)_+) P of a symmetric A = P^T diag(d) P is the nearest positive semidefinite matrix to A in the Frobenius norm, so it does not depend on the decomposition; it commutes with orthogonal conjugation, A = A_+ - (-A)_+ with <A_+, (-A)_+> = 0, A |-> A_+ is 1-Lipschitz, and (c A)_+ = c A_+ for c >= 0. <S, T> >= 0 for S, T >= 0 (mxdot_psd_ge0).

Used by 10 declarations in 1 file

this file: psd_partE, psd_part_psd, psd_part_nearest, psd_part_conj, psd_part_moreau, psd_part_nonexpansive, psd_partZ, trace_psd_part_shift, frobenius_psd_part_shift, mxdot_psd_part_shift

lemma psd_conj source, line 78

forall [R : realType] [n : nat] [P : 'M_n] [d : 'rV_n],
P \is orthogonalmx -> (forall i : 'I_n, 0 <= d 0 i) -> psdmx (P^T *m diag_mx d *m P)

Statement as written in the source

Lemma psd_conj n (P : 'M[R]_n) (d : 'rV[R]_n) : P \is orthogonalmx ->
  (forall i, 0 <= d 0 i) -> psdmx (P^T *m diag_mx d *m P).

Used by 5 declarations in 3 files

GaussianAnalysis.matrix.psd_splitting: spectral_nonneg_proj
this file: psd_nearest, psd_partE, psd_part_psd
GaussianAnalysis.random_matrix.matrix_series: psdmx_exp_even

lemma mxdot_psd_ge0 source, line 88

forall [R : realType] [n : nat] [S T : 'M_n], psdmx S -> psdmx T -> 0 <= mxdot S T

<S, T> >= 0 for S, T >= 0.

Statement as written in the source

Lemma mxdot_psd_ge0 n (S T : 'M[R]_n) : psdmx S -> psdmx T -> 0 <= mxdot S T.

Used by 5 declarations in 2 files

GaussianAnalysis.matrix.psd_splitting: mxtrace_psd_ge0, two_matrix_split, frobenius_sum_psd_le
this file: psd_nearest, psd_part_nonexpansive

lemma psd_nearest source, line 116

forall [R : realType] [n : nat] [P : 'M_n] (d : 'rV_n) [S : 'M_n],
P \is orthogonalmx ->
psdmx S ->
mxdot (P^T *m diag_mx d *m P - P^T *m diag_mx (pos_row d) *m P)
  (P^T *m diag_mx d *m P - P^T *m diag_mx (pos_row d) *m P) +
mxdot (P^T *m diag_mx (pos_row d) *m P - S) (P^T *m diag_mx (pos_row d) *m P - S) <=
mxdot (P^T *m diag_mx d *m P - S) (P^T *m diag_mx d *m P - S)

The decomposition A = A_+ - A_- for any spectral decomposition, with A_+, A_- >= 0 and <A_+, A_-> = 0, and the nearest-point inequality |A - S|^2 >= |A - A_+|^2 + |A_+ - S|^2 for S >= 0.

Statement as written in the source

Lemma psd_nearest n (P : 'M[R]_n) (d : 'rV[R]_n) (S : 'M[R]_n) :
  P \is orthogonalmx -> psdmx S ->
  mxdot (P^T *m diag_mx d *m P - S) (P^T *m diag_mx d *m P - S) >=
  mxdot (P^T *m diag_mx d *m P - P^T *m diag_mx (pos_row d) *m P)
        (P^T *m diag_mx d *m P - P^T *m diag_mx (pos_row d) *m P) +
  mxdot (P^T *m diag_mx (pos_row d) *m P - S)
        (P^T *m diag_mx (pos_row d) *m P - S).

Used by 2 declarations in 1 file

this file: psd_partE, psd_part_nearest

lemma psd_partE main result source, line 157

forall [R : realType] [n : nat] [A P : 'M_n] [d : 'rV_n],
P \is orthogonalmx ->
A = P^T *m diag_mx d *m P -> psd_part A = P^T *m diag_mx (pos_row d) *m P

psd_part does not depend on the spectral decomposition.

Main result

Stated in the README together with psd_part.

Statement as written in the source

Lemma psd_partE n (A P : 'M[R]_n) (d : 'rV[R]_n) :
  P \is orthogonalmx -> A = P^T *m diag_mx d *m P ->
  psd_part A = P^T *m diag_mx (pos_row d) *m P.

Used by 6 declarations in 1 file

this file: psd_part_conj, psd_part_moreau, psd_partZ, trace_psd_part_shift, frobenius_psd_part_shift, mxdot_psd_part_shift

lemma psd_part_psd source, line 185

forall [R : realType] [n : nat] (A : 'M_n), psdmx (psd_part A)

Statement as written in the source

Lemma psd_part_psd n (A : 'M[R]_n) : psdmx (psd_part A).

Used by 1 declaration in 1 file

this file: psd_part_nonexpansive

theorem psd_part_nearest main result source, line 191

forall [R : realType] [n : nat] [A S : 'M_n],
A \is symmetricmx -> psdmx S -> frobenius (A - psd_part A) <= frobenius (A - S)

The nearest positive semidefinite matrix.

Main result

Stated in the README together with psd_part.

Statement as written in the source

Theorem psd_part_nearest n (A S : 'M[R]_n) : A \is symmetricmx -> psdmx S ->
  frobenius (A - psd_part A) <= frobenius (A - S).

lemma psd_part_conj main result source, line 203

forall [R : realType] [n : nat] [A Q : 'M_n],
A \is symmetricmx ->
Q \is orthogonalmx -> psd_part (Q *m A *m Q^T) = Q *m psd_part A *m Q^T

Main result

Stated in the README together with psd_part.

Statement as written in the source

Lemma psd_part_conj n (A Q : 'M[R]_n) : A \is symmetricmx -> Q \is orthogonalmx ->
  psd_part (Q *m A *m Q^T) = Q *m psd_part A *m Q^T.

lemma psd_part_moreau main result source, line 220

forall [R : realType] [n : nat] [A : 'M_n],
A \is symmetricmx ->
A = psd_part A - psd_part (- A) /\ mxdot (psd_part A) (psd_part (- A)) = 0

Moreau's decomposition.

Main result

Stated in the README together with psd_part.

Statement as written in the source

Lemma psd_part_moreau n (A : 'M[R]_n) : A \is symmetricmx ->
  A = psd_part A - psd_part (- A) /\ mxdot (psd_part A) (psd_part (- A)) = 0.

Used by 1 declaration in 1 file

this file: psd_part_nonexpansive

lemma psd_part_nonexpansive main result source, line 247

forall [R : realType] [n : nat] [A B : 'M_n],
A \is symmetricmx ->
B \is symmetricmx -> frobenius (psd_part A - psd_part B) <= frobenius (A - B)

Main result

Stated in the README together with psd_part.

Statement as written in the source

Lemma psd_part_nonexpansive n (A B : 'M[R]_n) :
  A \is symmetricmx -> B \is symmetricmx ->
  frobenius (psd_part A - psd_part B) <= frobenius (A - B).

lemma psd_partZ main result source, line 274

forall [R : realType] [n : nat] [c : R] [A : 'M_n],
0 <= c -> A \is symmetricmx -> psd_part (c *: A) = c *: psd_part A

The positive part is positively homogeneous.

Main result

Stated in the README together with psd_part.

Statement as written in the source

Lemma psd_partZ n (c : R) (A : 'M[R]_n) : 0 <= c -> A \is symmetricmx ->
  psd_part (c *: A) = c *: psd_part A.

lemma spec_shift_decomposition source, line 289

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

A - w I = P^T diag (spec A - w) P.

Statement as written in the source

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

Used by 2 declarations in 1 file

this file: trace_psd_part_shift, frobenius_psd_part_shift

lemma trace_psd_part_shift main result source, line 302

forall [R : realType] [n : nat] [A : 'M_n] (w : R),
A \is symmetricmx -> \tr (psd_part (A - w%:M)) = \sum_i maxr (spec A 0 i - w) 0

The trace and the squared Frobenius norm of the shifted positive part, as spectral statistics.

Main result, as the README states it

tr (A - w I)_+ = sum_i (spec A i - w)_+, |(A - w I)_+|_F^2 = sum_i (spec A i - w)_+^2 and <A, (A - w I)_+> = sum_i spec A i (spec A i - w)_+, with the sorted eigenvalues spec of matrix/von_neumann.v.

Statement as written in the source

Lemma trace_psd_part_shift n (A : 'M[R]_n) (w : R) : A \is symmetricmx ->
  \tr (psd_part (A - w%:M)) = \sum_i Num.max (spec A 0 i - w) 0.

lemma frobenius_psd_part_shift main result source, line 310

forall [R : realType] [n : nat] [A : 'M_n] (w : R),
A \is symmetricmx ->
frobenius (psd_part (A - w%:M)) ^+ 2 = \sum_i maxr (spec A 0 i - w) 0 ^+ 2

Main result

Stated in the README together with trace_psd_part_shift.

Statement as written in the source

Lemma frobenius_psd_part_shift n (A : 'M[R]_n) (w : R) : A \is symmetricmx ->
  frobenius (psd_part (A - w%:M)) ^+ 2 = \sum_i Num.max (spec A 0 i - w) 0 ^+ 2.

The spectrum of conjugates of diagonal matrices.

sectionspec_conj

Variable R : realType.
Implicit Types n : nat.

lemma char_poly_conj_diag main result source, line 327

forall [R : realType] [n : nat] [P : 'M_n] (v : 'rV_n),
P \is orthogonalmx -> char_poly (P^T *m diag_mx v *m P) = \prod_i ('X - (v 0 i)%:P)

The characteristic polynomial of P^T diag(v) P, P orthogonal.

Main result, as the README states it

For P orthogonal, P^T diag(v) P has the characteristic polynomial prod_i (X - v_i), so its sorted spectrum is v when v is decreasing, and spec (c A) = c spec A for c >= 0. The eigenvalues of a positive semidefinite matrix are nonnegative and sum to the trace; von Neumann's inequality in the form <A, B> <= sum_i spec A i spec B i for A, B symmetric.

Statement as written in the source

Lemma char_poly_conj_diag n (P : 'M[R]_n) (v : 'rV[R]_n) :
  P \is orthogonalmx ->
  char_poly (P^T *m diag_mx v *m P) = \prod_i ('X - (v 0 i)%:P).

Used by 1 declaration in 1 file

this file: spec_conj_diag

lemma spec_conj_diag main result source, line 350

forall [R : realType] [n : nat] [P : 'M_n] [v : 'rV_n],
P \is orthogonalmx ->
(forall i j : 'I_n, (i <= j)%N -> v 0 j <= v 0 i) -> spec (P^T *m diag_mx v *m P) = v

The spectrum of P^T diag(v) P is v when v is decreasing: the characteristic polynomial determines the eigenvalues with their multiplicities.

Main result

Stated in the README together with char_poly_conj_diag.

Statement as written in the source

Lemma spec_conj_diag n (P : 'M[R]_n) (v : 'rV[R]_n) : P \is orthogonalmx ->
  (forall i j : 'I_n, (i <= j)%N -> v 0 j <= v 0 i) ->
  spec (P^T *m diag_mx v *m P) = v.

Used by 1 declaration in 1 file

this file: spec_scale

lemma spec_scale main result source, line 382

forall [R : realType] [n : nat] [A : 'M_n] [c : R],
A \is symmetricmx -> 0 <= c -> spec (c *: A) = c *: spec A

Main result

Stated in the README together with char_poly_conj_diag.

Statement as written in the source

Lemma spec_scale n (A : 'M[R]_n) (c : R) : A \is symmetricmx -> 0 <= c ->
  spec (c *: A) = c *: spec A.

Used by 1 declaration in 1 file

GaussianAnalysis.matrix.condition_cone: cond_energyZ

lemma spec_psd_ge0 main result source, line 392

forall [R : realType] [n : nat] [A : 'M_n] (i : 'I_n), psdmx A -> 0 <= spec A 0 i

Main result

Stated in the README together with char_poly_conj_diag.

Statement as written in the source

Lemma spec_psd_ge0 n (A : 'M[R]_n) i : psdmx A -> 0 <= spec A 0 i.

lemma sum_spec_trace main result source, line 398

forall [R : realType] [n : nat] [A : 'M_n], A \is symmetricmx -> \sum_i spec A 0 i = \tr A

Main result

Stated in the README together with char_poly_conj_diag.

Statement as written in the source

Lemma sum_spec_trace n (A : 'M[R]_n) : A \is symmetricmx ->
  \sum_i spec A 0 i = \tr A.

Used by 4 declarations in 1 file

GaussianAnalysis.matrix.condition_cone: cond_slice_t, cond_slice_spec, cond_slice_frobenius, cond_cone_slice

lemma mxdot_spec_le main result source, line 406

forall [R : realType] [n : nat] [A B : 'M_n],
A \is symmetricmx -> B \is symmetricmx -> mxdot A B <= \sum_i spec A 0 i * spec B 0 i

von Neumann's inequality for the Frobenius pairing.

Main result

Stated in the README together with char_poly_conj_diag.

Statement as written in the source

Lemma mxdot_spec_le n (A B : 'M[R]_n) :
  A \is symmetricmx -> B \is symmetricmx ->
  mxdot A B <= \sum_i spec A 0 i * spec B 0 i.

lemma mxdot_psd_part_shift main result source, line 415

forall [R : realType] [n : nat] [A : 'M_n] (w : R),
A \is symmetricmx ->
mxdot A (psd_part (A - w%:M)) = \sum_i spec A 0 i * maxr (spec A 0 i - w) 0

Main result

Stated in the README together with trace_psd_part_shift.

Statement as written in the source

Lemma mxdot_psd_part_shift n (A : 'M[R]_n) (w : R) : A \is symmetricmx ->
  mxdot A (psd_part (A - w%:M)) =
  \sum_i spec A 0 i * Num.max (spec A 0 i - w) 0.

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.