On this page

Orthogonal splitting of positive semidefinite matrices

GaussianAnalysis.matrix.psd_splittinglibrary/matrix/psd_splitting.v577 lines22 lemmas and theorems, 2 definitionssource

Imports 3 library modules and 8 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, mathcomp.reals.reals, mathcomp.algebra.arithmetic_tactic

Imported by 1

GaussianApplications.PsdSplittingTheorem

Target T5 of phase 12 (AGENTS.md, section Phase 12). A Rocq formalization of the credited argument of the lemma 'Orthogonal splitting' of 'Exponential PSD rank of positively shifted matching matrices' (family 126 of the OpenAI math collection, revision 1581d4cbd, source/sections/splitting.tex). The collection has no Lean version of it.

For positive semidefinite A_1, ..., A_L of 'M[R]_n, L >= 1, there are orthogonal projections P_1, ..., P_L, possibly zero, mutually orthogonal and of sum 1, such that the sum over z and s != z of |P_s A_z P_s|_F^2 is at most 2^(L-1) times the sum of tr (A_z A_z') over the ordered pairs of distinct indices.

The proof is the manuscript's. The two-matrix estimate: for A, B >= 0, the spectral projection P of A - B onto its nonnegative eigenspaces satisfies tr (A B) >= |P B P|_F^2 + |(1 - P) A (1 - P)|_F^2, because the off-diagonal blocks of A and B along P agree and the diagonal blocks are ordered. Then an induction on L, which splits A_1 from the sum of the others and applies the induction hypothesis to the compressions on the range of 1 - P. To keep the dimension fixed, the induction is relative to an orthogonal projection Q (psd_splitting_rel): the projections are below Q, they sum to Q, and the overlaps are tr (A_z Q A_z' Q). The squared triangle inequality on Q - P uses the nonnegative quadratic form X |-> tr (A X B X), and the spectral projection is built from symmetric_spectral and commutes with every matrix that commutes with A - B (diag_mx_commute_map), hence with Q.

Proved:

orthoprojmx1, orthoprojmx0, orthoprojmxB; psdmx_conj, psdmxD, psdmx_sum; mxtrace_psd_ge0 (tr (S T) >= 0 for S, T >= 0); frobenius_sqr_sym.
spectral_nonneg_proj: the spectral projection E of a symmetric M onto its nonnegative eigenspaces, with E M = M E, E M E >= 0, (1 - E) M (1 - E) <= 0, and X E = E X for every X that commutes with M.
mxdot_block0, mxdot_sym_tr, mxdot_compress: blocks along orthogonal projections; two_matrix_split: the two-matrix estimate, relative to Q.
frobenius_compress_le: compressing by projections of sum Q does not increase the Frobenius norm of a matrix supported by Q; frobenius_sum_psd_le: the squared norms of positive semidefinite matrices sum to at most the squared norm of their sum.
sum_offdiag_recl: a sum over the ordered pairs of distinct indices of 'I_L.+2 split at the first index; trace_quad_ge0, trace_quad_sub_le: tr (A (Q - P) B (Q - P)) <= 2 tr (A Q B Q) + 2 tr (A P B P).
psd_splitting_rel and psd_splitting: the lemma for L + 1 matrices, with constant 2^L.

`orthoprojmx P`	P is an orthogonal projection: symmetric and P P = P
`nonneg_part x`	1 if x >= 0 and 0 otherwise

Main results

Results	Statement
orthoprojmxspectral_nonneg_projmxtrace_psd_ge0frobenius_compress_lefrobenius_sum_psd_le	`orthoprojmx P`: `P` is symmetric with `P P = P`. For a symmetric `M`, the spectral projection `E` onto the nonnegative eigenspaces commutes with `M` and with every matrix that commutes with `M`, and `E M E >= 0 >= (1 - E) M (1 - E)`. `tr (S T) >= 0` for `S, T >= 0`. For orthogonal projections `P_s` of sum `Q` and `M = Q M Q`, `sum_s \|P_s M P_s\|_F^2 <= \|M\|_F^2`; for positive semidefinite `F_i`, `sum_i \|F_i\|_F^2 <= \|sum_i F_i\|_F^2`.
two_matrix_split	The two-matrix estimate, relative to an orthogonal projection `Q`: for `A, B >= 0` with `Q A Q = A` and `Q B Q = B`, the projection `P = Q E`, `E` the spectral projection of `A - B` onto its nonnegative eigenspaces, satisfies `P Q = Q P = P` and `\|P B P\|_F^2 + \|(Q - P) A (Q - P)\|_F^2 <= tr (A B)`.
psd_splitting_relpsd_splitting	Orthogonal splitting (the lemma of family 126 of the OpenAI math collection, target T5 of phase 12): for `L + 1` positive semidefinite matrices `A_z` and an orthogonal projection `Q`, there are orthogonal projections `P_s`, possibly zero, with `P_s P_t = 0` for `s != t`, `sum_s P_s = Q`, and `sum_z sum_(s != z) \|P_s A_z P_s\|_F^2 <= 2^L sum_z sum_(z' != z) tr (A_z Q A_z' Q)`; at `Q = 1` the overlaps are `tr (A_z A_z')`, summed over ordered pairs.

Declarations24 exported

sectionorthoprojmx

Variable R : realType.
Implicit Types n : nat.

definition orthoprojmx main result source, line 72

Type

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

Definition

Definition orthoprojmx n (P : 'M[R]_n) : Prop :=
  P \is symmetricmx /\ P *m P = P.

P is an orthogonal projection: symmetric and idempotent.

Main result, as the README states it

orthoprojmx P: P is symmetric with P P = P. For a symmetric M, the spectral projection E onto the nonnegative eigenspaces commutes with M and with every matrix that commutes with M, and E M E >= 0 >= (1 - E) M (1 - E). tr (S T) >= 0 for S, T >= 0. For orthogonal projections P_s of sum Q and M = Q M Q, sum_s |P_s M P_s|_F^2 <= |M|_F^2; for positive semidefinite F_i, sum_i |F_i|_F^2 <= |sum_i F_i|_F^2.

Used by 9 declarations in 1 file

this file: orthoprojmx1, orthoprojmx0, orthoprojmxB, spectral_nonneg_proj, two_matrix_split, mxdot_compress, frobenius_compress_le, psd_splitting_rel, psd_splitting

lemma orthoprojmx1 source, line 75

forall (R : realType) (n : nat), orthoprojmx (1%:M : 'M_n)

Statement as written in the source

Lemma orthoprojmx1 n : orthoprojmx (1%:M : 'M[R]_n).

Used by 1 declaration in 1 file

this file: psd_splitting

lemma orthoprojmx0 source, line 78

forall (R : realType) (n : nat), orthoprojmx (0 : 'M_n)

Statement as written in the source

Lemma orthoprojmx0 n : orthoprojmx (0 : 'M[R]_n).

lemma orthoprojmxB source, line 81

forall [R : realType] [n : nat] [Q P : 'M_n],
orthoprojmx Q -> orthoprojmx P -> P *m Q = P -> Q *m P = P -> orthoprojmx (Q - P)

Statement as written in the source

Lemma orthoprojmxB n (Q P : 'M[R]_n) : orthoprojmx Q -> orthoprojmx P ->
  P *m Q = P -> Q *m P = P -> orthoprojmx (Q - P).

Used by 2 declarations in 1 file

this file: two_matrix_split, psd_splitting_rel

lemma psdmx_conj source, line 90

forall [R : realType] [n : nat] [P M : 'M_n],
P \is symmetricmx -> psdmx M -> psdmx (P *m M *m P)

Statement as written in the source

Lemma psdmx_conj n (P M : 'M[R]_n) : P \is symmetricmx -> psdmx M ->
  psdmx (P *m M *m P).

Used by 3 declarations in 1 file

this file: two_matrix_split, trace_quad_ge0, psd_splitting_rel

lemma psdmxD source, line 99

forall [R : realType] [n : nat] [A B : 'M_n], psdmx A -> psdmx B -> psdmx (A + B)

Statement as written in the source

Lemma psdmxD n (A B : 'M[R]_n) : psdmx A -> psdmx B -> psdmx (A + B).

Used by 1 declaration in 1 file

this file: psdmx_sum

lemma psdmx0 source, line 107

forall (R : realType) (n : nat), psdmx (0 : 'M_n)

Statement as written in the source

Lemma psdmx0 n : psdmx (0 : 'M[R]_n).

Used by 1 declaration in 1 file

this file: psdmx_sum

lemma psdmx_sum source, line 112

forall [R : realType] [n : nat] [I : Type] (r : seq I) [P : pred I] [F : I -> 'M_n],
(forall i : I, P i -> psdmx (F i)) -> psdmx (\sum_(i <- r | P i) F i)

Statement as written in the source

Lemma psdmx_sum n I (r : seq I) (P : pred I) (F : I -> 'M[R]_n) :
  (forall i, P i -> psdmx (F i)) -> psdmx (\sum_(i <- r | P i) F i).

Used by 1 declaration in 1 file

this file: psd_splitting_rel

lemma mxtrace_psd_ge0 main result source, line 121

forall [R : realType] [n : nat] [S T : 'M_n], psdmx S -> psdmx T -> 0 <= \tr (S *m T)

The trace of a product of two positive semidefinite matrices is nonnegative.

Main result

Stated in the README together with orthoprojmx.

Statement as written in the source

Lemma mxtrace_psd_ge0 n (S T : 'M[R]_n) : psdmx S -> psdmx T ->
  0 <= \tr (S *m T).

Used by 2 declarations in 1 file

this file: trace_quad_ge0, psd_splitting_rel

lemma frobenius_sqr_sym source, line 128

forall [R : realType] [n : nat] [M : 'M_n],
M \is symmetricmx -> frobenius M ^+ 2 = \tr (M *m M)

Statement as written in the source

Lemma frobenius_sqr_sym n (M : 'M[R]_n) : M \is symmetricmx ->
  frobenius M ^+ 2 = \tr (M *m M).

sectionspectral_projection

Variable R : realType.
Implicit Types n : nat.

lemma diag_mx_commute_map source, line 139

forall [R : realType] [n : nat] [X : 'M_n] [d : 'rV_n] (f : R -> R),
X *m diag_mx d = diag_mx d *m X ->
X *m diag_mx (d ^ f)%sesqui = diag_mx (d ^ f)%sesqui *m X

A matrix that commutes with diag_mx d commutes with diag_mx (f d).

Statement as written in the source

Lemma diag_mx_commute_map n (X : 'M[R]_n) (d : 'rV[R]_n) (f : R -> R) :
  X *m diag_mx d = diag_mx d *m X ->
  X *m diag_mx (map_mx f d) = diag_mx (map_mx f d) *m X.

Used by 1 declaration in 1 file

this file: spectral_nonneg_proj

definition nonneg_part source, line 150

Type

forall [R : realType], R -> R

Definition

Definition nonneg_part (x : R) : R := if 0 <= x then 1 else 0.

Used by 1 declaration in 1 file

this file: spectral_nonneg_proj

lemma spectral_nonneg_proj main result source, line 155

forall [R : realType] [n : nat] [M : 'M_n],
M \is symmetricmx ->
exists E : 'M_n,
  [/\ orthoprojmx E, E *m M = M *m E, psdmx (E *m M *m E),
      psdmx (- ((1%:M - E) *m M *m (1%:M - E)))
    & forall X : 'M_n, X *m M = M *m X -> X *m E = E *m X]

The spectral projection of a symmetric matrix M onto its nonnegative eigenspaces: an orthogonal projection E commuting with M and with every matrix that commutes with M, with E M E >= 0 and (1 - E) M (1 - E) <= 0.

Main result

Stated in the README together with orthoprojmx.

Statement as written in the source

Lemma spectral_nonneg_proj n (M : 'M[R]_n) : M \is symmetricmx ->
  exists E : 'M[R]_n,
  [/\ orthoprojmx E, E *m M = M *m E,
      psdmx (E *m M *m E), psdmx (- ((1%:M - E) *m M *m (1%:M - E))) &
      forall X : 'M[R]_n, X *m M = M *m X -> X *m E = E *m X].

Used by 1 declaration in 1 file

this file: two_matrix_split

sectiontwo_matrix

Variable R : realType.
Implicit Types n : nat.

lemma mxdot_block0 source, line 230

forall [R : realType] [n : nat] [P1 Q1 P2 Q2 : 'M_n] (M N : 'M_n),
P1 \is symmetricmx ->
Q2 \is symmetricmx ->
P1 *m P2 = 0 \/ Q1 *m Q2 = 0 -> mxdot (P1 *m M *m Q1) (P2 *m N *m Q2) = 0

Blocks along orthogonal projections are orthogonal for mxdot.

Statement as written in the source

Lemma mxdot_block0 n (P1 Q1 P2 Q2 M N : 'M[R]_n) :
  P1 \is symmetricmx -> Q2 \is symmetricmx ->
  P1 *m P2 = 0 \/ Q1 *m Q2 = 0 ->
  mxdot (P1 *m M *m Q1) (P2 *m N *m Q2) = 0.

lemma mxdot_sym_tr source, line 242

forall [R : realType] [n : nat] (A : 'M_n) [B : 'M_n],
B \is symmetricmx -> mxdot A B = \tr (A *m B)

Statement as written in the source

Lemma mxdot_sym_tr n (A B : 'M[R]_n) : B \is symmetricmx ->
  mxdot A B = \tr (A *m B).

Used by 2 declarations in 1 file

this file: two_matrix_split, psd_splitting_rel

lemma two_matrix_split main result source, line 251

forall [R : realType] [n : nat] [Q A B : 'M_n],
orthoprojmx Q ->
psdmx A ->
psdmx B ->
Q *m A *m Q = A ->
Q *m B *m Q = B ->
exists P : 'M_n,
  [/\ orthoprojmx P, P *m Q = P, Q *m P = P
    & frobenius (P *m B *m P) ^+ 2 + frobenius ((Q - P) *m A *m (Q - P)) ^+ 2 <=
      \tr (A *m B)]

The two-matrix estimate of the lemma 'Orthogonal splitting', relative to an orthogonal projection Q: for A, B >= 0 with Q A Q = A and Q B Q = B, the projection P = Q E, with E the spectral projection of A - B onto its nonnegative eigenspaces, satisfies P <= Q and |P B P|_F^2 + |(Q - P) A (Q - P)|_F^2 <= tr (A B).

Main result, as the README states it

The two-matrix estimate, relative to an orthogonal projection Q: for A, B >= 0 with Q A Q = A and Q B Q = B, the projection P = Q E, E the spectral projection of A - B onto its nonnegative eigenspaces, satisfies P Q = Q P = P and |P B P|_F^2 + |(Q - P) A (Q - P)|_F^2 <= tr (A B).

Statement as written in the source

Lemma two_matrix_split n (Q A B : 'M[R]_n) :
  orthoprojmx Q -> psdmx A -> psdmx B ->
  Q *m A *m Q = A -> Q *m B *m Q = B ->
  exists P : 'M[R]_n,
  [/\ orthoprojmx P, P *m Q = P, Q *m P = P &
      frobenius (P *m B *m P) ^+ 2 +
      frobenius ((Q - P) *m A *m (Q - P)) ^+ 2 <= \tr (A *m B)].

Used by 1 declaration in 1 file

this file: psd_splitting_rel

sectionsplitting

Variable R : realType.
Implicit Types n : nat.

lemma mxdot_compress source, line 342

forall [R : realType] [n : nat] [K1 K2 : 'M_n] (X Y : 'M_n),
orthoprojmx K1 ->
orthoprojmx K2 -> mxdot (K1 *m X *m K2) (K1 *m Y *m K2) = mxdot X (K1 *m Y *m K2)

Statement as written in the source

Lemma mxdot_compress n (K1 K2 X Y : 'M[R]_n) : orthoprojmx K1 -> orthoprojmx K2 ->
  mxdot (K1 *m X *m K2) (K1 *m Y *m K2) = mxdot X (K1 *m Y *m K2).

Used by 2 declarations in 1 file

this file: frobenius_compress_le, psd_splitting_rel

lemma frobenius_compress_le main result source, line 352

forall [R : realType] [n : nat] [I : finType] [P : I -> 'M_n] [Q M : 'M_n],
(forall s : I, orthoprojmx (P s)) ->
\sum_s P s = Q ->
Q *m M *m Q = M -> \sum_s frobenius (P s *m M *m P s) ^+ 2 <= frobenius M ^+ 2

Compressing by a family of orthogonal projections that sums to Q does not increase the Frobenius norm of a matrix supported by Q.

Main result

Stated in the README together with orthoprojmx.

Statement as written in the source

Lemma frobenius_compress_le n (I : finType) (P : I -> 'M[R]_n) (Q M : 'M[R]_n) :
  (forall s, orthoprojmx (P s)) -> \sum_s P s = Q -> Q *m M *m Q = M ->
  \sum_s frobenius (P s *m M *m P s) ^+ 2 <= frobenius M ^+ 2.

Used by 1 declaration in 1 file

this file: psd_splitting_rel

lemma frobenius_sum_psd_le main result source, line 368

forall [R : realType] [n : nat] [I : finType] [F : I -> 'M_n],
(forall i : I, psdmx (F i)) -> \sum_i frobenius (F i) ^+ 2 <= frobenius (\sum_i F i) ^+ 2

For positive semidefinite F i, the sum of the squared norms is at most the squared norm of the sum.

Main result

Stated in the README together with orthoprojmx.

Statement as written in the source

Lemma frobenius_sum_psd_le n (I : finType) (F : I -> 'M[R]_n) :
  (forall i, psdmx (F i)) ->
  \sum_i frobenius (F i) ^+ 2 <= frobenius (\sum_i F i) ^+ 2.

Used by 1 declaration in 1 file

this file: psd_splitting_rel

lemma sum_offdiag_recl source, line 379

forall [V : GRing.Nmodule.Exports.nmodType] [L : nat] (F : 'I_L.+2 -> 'I_L.+2 -> V),
\sum_z \sum_(s | s != z) F z s =
\sum_j F ord0 (lift ord0 j) + \sum_j F (lift ord0 j) ord0 +
\sum_j \sum_(i | i != j) F (lift ord0 j) (lift ord0 i)

A sum over the ordered pairs of distinct indices of 'I_L.+2, split at the index ord0.

Statement as written in the source

Lemma sum_offdiag_recl (V : nmodType) L (F : 'I_L.+2 -> 'I_L.+2 -> V) :
  \sum_z \sum_(s | s != z) F z s =
  \sum_j F ord0 (lift ord0 j) + \sum_j F (lift ord0 j) ord0 +
  \sum_j \sum_(i | i != j) F (lift ord0 j) (lift ord0 i).

Used by 1 declaration in 1 file

this file: psd_splitting_rel

lemma trace_quad_ge0 source, line 394

forall [R : realType] [n : nat] [A B X : 'M_n],
psdmx A -> psdmx B -> X \is symmetricmx -> 0 <= \tr (A *m X *m B *m X)

Statement as written in the source

Lemma trace_quad_ge0 n (A B X : 'M[R]_n) : psdmx A -> psdmx B ->
  X \is symmetricmx -> 0 <= \tr (A *m X *m B *m X).

Used by 2 declarations in 1 file

this file: trace_quad_sub_le, psd_splitting_rel

lemma trace_quad_sub_le source, line 403

forall [R : realType] [n : nat] [A B Q P : 'M_n],
psdmx A ->
psdmx B ->
Q \is symmetricmx ->
P \is symmetricmx ->
\tr (A *m (Q - P) *m B *m (Q - P)) <=
2 * \tr (A *m Q *m B *m Q) + 2 * \tr (A *m P *m B *m P)

The squared triangle inequality for the nonnegative quadratic form X |-> tr (A X B X) on symmetric matrices.

Statement as written in the source

Lemma trace_quad_sub_le n (A B Q P : 'M[R]_n) : psdmx A -> psdmx B ->
  Q \is symmetricmx -> P \is symmetricmx ->
  \tr (A *m (Q - P) *m B *m (Q - P)) <=
  2 * \tr (A *m Q *m B *m Q) + 2 * \tr (A *m P *m B *m P).

Used by 1 declaration in 1 file

this file: psd_splitting_rel

theorem psd_splitting_rel main result source, line 423

forall [R : realType] [n L : nat] [Q : 'M_n] [A : 'I_L.+1 -> 'M_n],
orthoprojmx Q ->
(forall z : 'I_L.+1, psdmx (A z)) ->
exists P : 'I_L.+1 -> 'M_n,
  [/\ forall s : 'I_L.+1, orthoprojmx (P s),
      forall s t : 'I_L.+1,
      s != t -> P s *m P t = 0,
      \sum_s P s = Q
    & \sum_z \sum_(s | s != z) frobenius (P s *m A z *m P s) ^+ 2 <=
      2 ^+ L * \sum_z \sum_(z' | z' != z) \tr (A z *m Q *m A z' *m Q)]

The lemma 'Orthogonal splitting', relative to an orthogonal projection Q: for L + 1 positive semidefinite matrices, orthogonal projections P_s that sum to Q, with constant 2^L for the overlaps tr (A_z Q A_z' Q).

Main result, as the README states it

Orthogonal splitting (the lemma of family 126 of the OpenAI math collection, target T5 of phase 12): for L + 1 positive semidefinite matrices A_z and an orthogonal projection Q, there are orthogonal projections P_s, possibly zero, with P_s P_t = 0 for s != t, sum_s P_s = Q, and sum_z sum_(s != z) |P_s A_z P_s|_F^2 <= 2^L sum_z sum_(z' != z) tr (A_z Q A_z' Q); at Q = 1 the overlaps are tr (A_z A_z'), summed over ordered pairs.

Statement as written in the source

Theorem psd_splitting_rel n L (Q : 'M[R]_n) (A : 'I_L.+1 -> 'M[R]_n) :
  orthoprojmx Q -> (forall z, psdmx (A z)) ->
  exists P : 'I_L.+1 -> 'M[R]_n,
  [/\ forall s, orthoprojmx (P s),
      forall s t, s != t -> P s *m P t = 0,
      \sum_s P s = Q &
      \sum_z \sum_(s | s != z) frobenius (P s *m A z *m P s) ^+ 2 <=
        2 ^+ L * \sum_z \sum_(z' | z' != z) \tr (A z *m Q *m A z' *m Q)].

Used by 1 declaration in 1 file

this file: psd_splitting

theorem psd_splitting main result source, line 564

forall [R : realType] [n L : nat] [A : 'I_L.+1 -> 'M_n],
(forall z : 'I_L.+1, psdmx (A z)) ->
exists P : 'I_L.+1 -> 'M_n,
  [/\ forall s : 'I_L.+1, orthoprojmx (P s),
      forall s t : 'I_L.+1,
      s != t -> P s *m P t = 0,
      \sum_s P s = 1%:M
    & \sum_z \sum_(s | s != z) frobenius (P s *m A z *m P s) ^+ 2 <=
      2 ^+ L * \sum_z \sum_(z' | z' != z) \tr (A z *m A z')]

The lemma 'Orthogonal splitting': for L + 1 positive semidefinite matrices A_z, orthogonal projections P_s, possibly zero, that are mutually orthogonal and sum to the identity, with the sum over z and s != z of |P_s A_z P_s|_F^2 at most 2^L times the sum over the ordered pairs z != z' of tr (A_z A_z').

Main result

Stated in the README together with psd_splitting_rel.

Statement as written in the source

Theorem psd_splitting n L (A : 'I_L.+1 -> 'M[R]_n) : (forall z, psdmx (A z)) ->
  exists P : 'I_L.+1 -> 'M[R]_n,
  [/\ forall s, orthoprojmx (P s),
      forall s t, s != t -> P s *m P t = 0,
      \sum_s P s = 1%:M &
      \sum_z \sum_(s | s != z) frobenius (P s *m A z *m P s) ^+ 2 <=
        2 ^+ L * \sum_z \sum_(z' | z' != z) \tr (A z *m A z')].

Used by 1 declaration in 1 file

GaussianApplications.PsdSplittingTheorem: psd_splitting_theorem

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.