On this page
Effective rank of a weighted sum of rank-one matrices
Imports 3 library modules and 12 external
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.matrix.real_spectral
- GaussianAnalysis.matrix.von_neumann
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.classical.boolp, mathcomp.classical.classical_sets, mathcomp.reals.reals, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic
Required by 1 files of the paper proofs
Let u_1, ..., u_n be row vectors of R^p whose rank-one matrices u_i^T u_i are close to the identity in the sense that
sum_i <u_i^T u_i - I, A>^2 <= L^2 |A|_F^2 for every p x p matrix A,
and let t be weights with |t| = 1 and 8 L^2 t_i^2 <= k for every i, with 0 < k <= p. Then Sigma_t = sum_i t_i^2 u_i^T u_i has fewer than k eigenvalues below 1/8: its sorted eigenvalues spec Sigma_t (von_neumann.v) are at least 1/8 at every index j with j + k <= p (effective_rank_spec).
This is the deterministic part of Lemma 3.12 of Koehler and Sohn (arXiv 2608.27372, lines 3314-3405 of arxiv_v1.tex), where the hypothesis comes from the a priori estimate of the features (u_i u_i^T - I) / sqrt p. The proof is the paper's: if k eigenvalues were below 1/8, the projection H on their eigenvectors would give <H, Sigma_t> < k / 8, while the hypothesis at A = H, which has |H|_F^2 = tr H = k, bounds the weight of the points with u_i H u_i^T < k / 2, and gives <H, Sigma_t> >= k / 4.
Main results
| Results | Statement |
|---|---|
Effective rank of a weighted sum of rank-one matrices (the deterministic part of Lemma 3.12 of Koehler and Sohn): if u_1, ..., u_n in 'rV_p satisfy sum_i <u_i^T u_i - I, A>^2 <= L^2 |A|_F^2 for every A, and |t| = 1 with 8 L^2 t_i^2 <= k for every i, 0 < k <= p, then Sigma_t = sum_i t_i^2 u_i^T u_i has fewer than k eigenvalues below 1/8: spec Sigma_t j >= 1/8 whenever j + k <= p. |
Declarations1 exported
Variable R : realType.
forall [R : realType] [n p : nat] [u : 'I_n -> 'rV_p] [t : 'rV_n] [L : R] [k : nat], (forall A : 'M_p, \sum_i mxdot ((u i)^T *m u i - 1%:M) A ^+ 2 <= L ^+ 2 * mxdot A A) -> (0 < k)%N -> (k <= p)%N -> mxdot t t = 1 -> (forall i : 'I_n, 8 * L ^+ 2 * t 0 i ^+ 2 <= k%:R) -> forall [j : 'I_p], (j + k <= p)%N -> 8^-1 <= spec (\sum_i t 0 i ^+ 2 *: ((u i)^T *m u i)) 0 j
Effective rank of a weighted sum of rank-one matrices (the deterministic part of Lemma 3.12 of Koehler and Sohn): if u_1, ..., u_n in 'rV_p satisfy sum_i <u_i^T u_i - I, A>^2 <= L^2 |A|_F^2 for every A, and |t| = 1 with 8 L^2 t_i^2 <= k for every i, 0 < k <= p, then Sigma_t = sum_i t_i^2 u_i^T u_i has fewer than k eigenvalues below 1/8: spec Sigma_t j >= 1/8 whenever j + k <= p.
Statement as written in the source
Lemma effective_rank_spec n p (u : 'I_n -> 'rV[R]_p) (t : 'rV[R]_n) (L : R) (k : nat) : (forall A : 'M[R]_p, \sum_i mxdot ((u i)^T *m u i - 1%:M) A ^+ 2 <= L ^+ 2 * mxdot A A) -> (0 < k)%N -> (k <= p)%N -> mxdot t t = 1 -> (forall i, 8 * L ^+ 2 * t 0 i ^+ 2 <= k%:R) -> forall j : 'I_p, (j + k <= p)%N -> 8^-1 <= spec (\sum_i t 0 i ^+ 2 *: ((u i)^T *m u i)) 0 j.