On this page
Orthogonal splitting of positive semidefinite matrices: the theorem
Imports 4 library modules and 7 external
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.matrix.psd_part
- GaussianAnalysis.matrix.psd_splitting
- GaussianApplications.PsdSplittingStatement
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
Target T5 of phase 12 (AGENTS.md, section Phase 12). psd_splitting_theorem proves psd_splitting_statement of PsdSplittingStatement.v, 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), from psd_splitting of library/matrix/psd_splitting.v, a Rocq formalization of the credited argument. The statement indexes L >= 1 matrices by 'I_L; the library lemma takes L + 1 matrices, with constant 2^L.
Main results
| Results | Statement |
|---|---|
Proves psd_splitting_statement (T5): for every R : realType, L >= 1 and positive semidefinite A_1, ..., A_L of 'M[R]_n, there are orthogonal projections P_1, ..., P_L, possibly zero, with P_s P_t = 0 for s != t and sum_s P_s = 1, and sum_z sum_(s != z) |P_s A_z P_s|_F^2 <= 2^(L-1) sum_z sum_(z' != z) tr (A_z A_z'), from psd_splitting of library/. |
Declarations1 exported
Proves psd_splitting_statement (T5): for every R : realType, L >= 1 and positive semidefinite A_1, ..., A_L of 'M[R]_n, there are orthogonal projections P_1, ..., P_L, possibly zero, with P_s P_t = 0 for s != t and sum_s P_s = 1, and sum_z sum_(s != z) |P_s A_z P_s|_F^2 <= 2^(L-1) sum_z sum_(z' != z) tr (A_z A_z'), from psd_splitting of library/.
Statement as written in the source
Theorem psd_splitting_theorem : psd_splitting_statement.