On this page
GaussianAnalysismatrix/
matrix/
The spectral theorem for real symmetric matrices, the positive part of a symmetric matrix and whitening, operator, Frobenius and nuclear norms, nets on spheres and coverings of nuclear-norm balls, von Neumann's trace inequality and the Hoffman-Wielandt inequality, the cone of matrices of bounded condition number, its distance and support function, the maximizer of a trace-penalized quadratic on a closed convex set of matrices, effective ranks, the operator norm of sums of independent random matrices, the largest eigenvalue as the supremum of the quadratic form on the unit sphere, the orthogonal splitting of positive semidefinite matrices.
Guide
Written for this documentation from the sources and the README, and checked against the Rocq statements. The file headers and the statements are the reference.
This directory is the linear algebra of the library: real matrices over an arbitrary realType, with vectors as row or column matrices, the Frobenius inner product mxdot, written <A, B>, and its norm frobenius, written |A|.
The base is the spectral theorem for real symmetric matrices, proved without complex numbers. On it rest operator norms, the largest eigenvalue, sorted spectra, positive parts, nuclear norms, nets, convex sets, coverings and random matrices. Four files serve targets T2 to T5 of applications/.
Reading order
euclidean.v: the Frobenius inner product and norm, orthogonal matrices.real_spectral.v: Householder reflections and the spectral theorem.opnorm.v: the operator norm.whitening.v: whitening a symmetric S >= b I, b > 0.lambda_max.v: the largest eigenvalue.spectral_gap.v: a spectral gap from the square, and the Schur test.nets.v: eps-nets, and operator norms read on nets.von_neumann.v: the sorted spectrum, von Neumann's and Hoffman-Wielandt's inequalities.psd_part.v: the positive part of a symmetric matrix.psd_splitting.v: orthogonal splitting of positive semidefinite matrices.nuclear.v: the nuclear norm and the range duality.condition_cone.v: the cone of matrices of bounded condition number.trace_projection.v: maximizing a trace-penalized quadratic on a closed convex set.effective_rank.v: few small eigenvalues in a weighted sum of rank-one matrices.random_opnorm.v: the operator norm of sums of independent random matrices.covering.v: coverings of nuclear-norm balls by products of column balls.tensor_packing.v: tensor packing.
Core definitions
mxdot,frobenius(euclidean.v): sum_i sum_j A_ij B_ij and sqrt <A, A>.sym_spectralmx,sym_spectral_diag(real_spectral.v): a chosen orthogonal P and row d with A = P^T diag(d) P when A is symmetric.opnorm(opnorm.v): the supremum of |A x| over |x| <= 1.lambda_max(lambda_max.v): the supremum of x^T A x over unit x (0 when n = 0), an eigenvalue for symmetric A when n > 0; frozen with target T3.spec(von_neumann.v): the eigenvalues of a symmetric matrix in decreasing order.psdmx,psd_part(psd_part.v): A symmetric with x^T A x >= 0; the positive part P^T diag((d_i)_+) P.nuclear(nuclear.v): the supremum of <A, B> over opnorm B <= 1.cond_cone,cond_dist(condition_cone.v): the symmetric Q with t I <= Q <= C t I for some t >= 0; the infimum over t >= 0 of sum_i dist(spec H i, [t, C t])^2.trace_quad,trace_argmax(trace_projection.v): 2 <H, S> - |S|^2 - (c / n) (tr S)^2, and its maximizer on K.
Main results
Spectra and norms.
symmetric_spectral: every symmetric A is P^T diag(d) P with P orthogonal.opnorm_leP,opnorm_spectral: for b >= 0, opnorm A <= b iff |A x| <= b |x| for all x; for A = P^T diag(d) P with P orthogonal, opnorm A = max_i |d_i|.von_neumann_trace,hoffman_wielandt: for A, B symmetric, tr(A B) <= sum_i spec A i spec B i and sum_i (spec A i - spec B i)^2 <= |A - B|^2.
Duality and convex sets.
range_duality: for W_1, ..., W_k in 'M_n and M >= 0, if |<l, y>| <= M nuclear (sum_i l_i W_i) for all l, then y = (<W_i, D>)_i for some D with opnorm D <= M.cond_cone_dist: for C >= 1 and H symmetric, the infimum of |H - Q|^2 over Q in cond_cone C is cond_dist C H.trace_argmaxP,trace_argmax_ge: for c > -1 and K nonempty, convex and closed in the coordinates of mxvec, X = trace_argmax K c H lies in K and trace_quad c H S + min(1, 1 + c) |S - X|^2 <= trace_quad c H X on K.
Nets and random matrices.
net_exists: for r >= 0 and eps > 0, every set in the radius-r ball of 'cV_n has an eps-net of at most (2 e (1 + 2 r / eps))^n of its points.opnorm_sum_subexponential: for x of law tuple_prod mu n and m x m matrices Y with forms v^T Y v, |v| <= 1, centered and subexponential with constant L > 0 under each mu k, the symmetric part of sum_k a_k Y(x_k), |a_k| <= 1, has operator norm below a measurable N a with E N a <= 96 L (sqrt (n (m + 1)) + m + 1).product_covering: for c0, gam > 0, an integer d > 0 and m, q in [c0 d, C0 d], a set of m x q matrices A with <A, B> <= gam d opnorm B for all B is covered by at most exp((96 C0 + 33) / c0^2)^(m q) balls of radius gam for the largest column norm.
Targets of applications/.
psd_splitting(T5): for L + 1 positive semidefinite A_z, some orthogonal projections P_s of sum 1, with P_s P_t = 0 for s != t, satisfy sum_z sum_(s != z) |P_s A_z P_s|^2 <= 2^L sum_z sum_(z' != z) tr(A_z A_z').tensor_packing(T2): for x_a, y_a in the unit balls with |<x_a, x_b>|, |<y_a, y_b>| <= eta for a != b outside relations Gx, Gy with at most L successors per vertex, Frobenius-orthonormal A_1, ..., A_r with r <= d, d >= 1, 0 < eps <= 1 and 0 <= eta <= eps^2 / 10^4, at most 30000 (1 + L) / eps^2 exp(30000 sqrt d ln(2 + d) / eps^2) indices have sum_k (x_a A_k y_a^T)^2 >= eps^2.psd_square_gap,opnorm_row_sum(T4): for B symmetric positive semidefinite with k x^T B x <= |B x|^2 for all x, k |x|^2 <= x^T B x on the orthogonal of the kernel; for B symmetric, rho >= 0 and every sum_j |B_ij| <= rho, opnorm B <= rho.
How the proofs go
symmetric_spectral: the quadratic form is maximal on the compact unit sphere at an eigenvector; a Householder reflection splits off a dimension.von_neumann_trace: the squared entries of an orthogonal matrix form a doubly stochastic matrix; Abel summation concludes without Birkhoff's theorem.range_dualityprojects y on the image of the operator-norm ball (convex/).moreau.v product_coveringrests on Sudakov's minoration and its dual, not on Urysohn's inequality.tensor_packingcuts two spectra at sqrt d, bounds clusters of almost orthogonal vectors, then applies Sudakov's minoration andgauss_mx_series_opnorm_log.
Connections
The first ten files and effective_rank.v need only MathComp, MathComp-Analysis and this directory; the other six draw on gaussian/, convex/, probability/, comparison/, fourier/ and random_matrix/.
Every other library directory requires euclidean.v, and random_matrix/ six more files. theories/ and extension/ use the directory at Stdlib's reals; applications/ uses it for targets T1 to T5.
Files
| File | Title | Lines | Lemmas | Defs | Requires in this directory |
|---|---|---|---|---|---|
| euclidean.v | The Euclidean structure of real matrices | 363 | 60 | 3 | none |
| real_spectral.v | The spectral theorem for real symmetric matrices | 476 | 35 | 3 | euclidean |
| whitening.v | Whitening | 113 | 4 | 1 | euclidean, real_spectral |
| opnorm.v | The operator norm of real matrices | 304 | 27 | 1 | euclidean, real_spectral |
| lambda_max.v | The largest eigenvalue of a real square matrix | 220 | 16 | 1 | euclidean, real_spectral, opnorm |
| psd_splitting.v | Orthogonal splitting of positive semidefinite matrices | 577 | 22 | 2 | euclidean, real_spectral, psd_part |
| spectral_gap.v | Two bounds for real symmetric matrices | 114 | 4 | 0 | euclidean, real_spectral, opnorm |
| nets.v | Nets in Euclidean spaces | 471 | 28 | 8 | euclidean, real_spectral, opnorm |
| random_opnorm.v | The operator norm of a sum of independent random matrices | 524 | 13 | 1 | euclidean, real_spectral, opnorm, nets |
| covering.v | Covering the nuclear-norm ball by products of column balls | 508 | 14 | 2 | euclidean, opnorm |
| von_neumann.v | Von Neumann's trace inequality and the Hoffman-Wielandt inequality | 395 | 21 | 2 | euclidean, real_spectral |
| psd_part.v | The positive part of a symmetric matrix | 430 | 20 | 3 | euclidean, real_spectral, von_neumann |
| effective_rank.v | Effective rank of a weighted sum of rank-one matrices | 152 | 1 | 0 | euclidean, real_spectral, von_neumann |
| nuclear.v | The nuclear norm and the range duality | 409 | 20 | 3 | euclidean, real_spectral, opnorm |
| condition_cone.v | The cone of matrices of bounded condition number | 785 | 47 | 10 | euclidean, real_spectral, opnorm, von_neumann, psd_part, nuclear |
| trace_projection.v | The maximizer of a trace-penalized quadratic on a closed convex set | 443 | 28 | 3 | euclidean |
| tensor_packing.v | Tensor packing | 1,214 | 50 | 4 | euclidean, opnorm, real_spectral, psd_part, nets |
Table of main results48 rows of the README
| File | Results | Statement | Used by theories/ |
|---|---|---|---|
| euclidean.v | mxdot A B, the sum of the A_(i, j) B_(i, j), is the Frobenius inner product of real matrices and frobenius A its norm. Cauchy-Schwarz holds, and the norm satisfies the triangle inequality and is submultiplicative. On row and column vectors they are the Euclidean inner product and norm. | Spectral/, Spectral/, Feature/, SquareFree/, SquareFree/, Gaussian/, Gaussian/, Gaussian/, Gaussian/, Gordon/, Gordon/; in the library, the nine files of comparison/ that handle vectors. mxdot_cauchy_schwarz and frobeniusD are used inside the library only | |
The orthogonal matrices (M M^T = 1). Multiplying by an orthogonal matrix, on either side, preserves the Frobenius inner product and norm. | Spectral/, Spectral/ | ||
| real_ | Spectral theorem: every real symmetric matrix is P^T diag(d) P with P orthogonal, over any realType. Proved by maximizing the quadratic form on the unit sphere and splitting off a dimension with a Householder reflection. | Spectral/ | |
mx_norm A <= frobenius A <= sqrt (m n) mx_norm A, where mx_norm is the norm of MathComp-Analysis on matrices (the largest absolute value of an entry), so the Frobenius norm defines the topology of 'M[R]_(m, n); the unit sphere of 'rV[R]_n is compact. | through symmetric_spectral | ||
| The quadratic form attains its maximum on the unit sphere; for a symmetric matrix a maximizer is an eigenvector. | through symmetric_spectral | ||
If A = P^T diag(d) P with P orthogonal: the trace is the sum of the d_i, the squared Frobenius norm is the sum of the d_i^2, x^T A x = sum_i d_i (P x)_i^2, and x^T A x <= b x^T x for all x if and only if every d_i <= b (likewise for lower bounds, positive semidefiniteness and absolute values). | Spectral/, Spectral/; spectral_form_le inside the library only | ||
If A = P^T diag(d) P with P orthogonal, then A^k = P^T diag(d^k) P. For symmetric A, B: tr(ABAB) <= tr(A^2 B^2). | Feature/; spectral_exp inside the library only | ||
| whitening.v | Whitening: if S is symmetric and b |x|^2 <= x S x^T for all row vectors x, with b > 0, then the eigenvalues of S are at least b, and W = diag(d)^(-1/2) P, for the spectral decomposition S = P^T diag(d) P, satisfies W S W^T = 1 and |x W| <= |x| / sqrt b. | ||
The case b = 1: a symmetric S with |x|^2 <= x S x^T has a W with W S W^T = 1 and |x W| <= |x| for all x. | |||
| opnorm.v | The operator norm sup_{|x| <= 1} |A x| is the least b with |A x| <= b |x|, and the least b with |y^T A x| <= b |y| |x|. It is a submultiplicative norm, invariant under transposition and orthogonal multiplication, and lies between the entrywise norm mx_norm of MathComp-Analysis and the Frobenius norm (mx_norm_le_opnorm, opnorm_le_frobenius). | Spectral/, SquareFree/, SquareFree/, Head/; opnorm_trmx inside the library only | |
For a symmetric matrix, opnorm A <= b if and only if |x^T A x| <= b x^T x for all x, and the operator norm is the largest absolute value of an eigenvalue. | Feature/, SquareFree/, SquareFree/, Spectral/, Spectral/, Head/ | ||
For a symmetric matrix and an even exponent p > 0, opnorm A ^ p <= tr(A^p); so tr(A^p) <= t^p with t >= 0 gives opnorm A <= t, and so does x^T A^p x <= t^p x^T x for all x. | Feature/, SquareFree/, SquareFree/, SquareFree/ | ||
| lambda_ | lambda_max A, the supremum of x^T A x over the unit columns x of a square matrix (0 when n = 0). It bounds x^T A x for unit x, and x^T A x <= lambda_max A x^T x for all x; for n > 0 it is the least such bound and is attained at a unit vector. The definition is alone in its section, frozen with the statement of target T3 of phase 12 (applications/, accepted at fc76edf). | ||
For n > 0 and A symmetric, lambda_max A is an eigenvalue of A with a unit eigenvector. For every square A, every eigenvalue of A with a unit eigenvector is at most lambda_max A. | |||
lambda_max A <= opnorm A, lambda_max (A + B) <= lambda_max A + lambda_max B, and |lambda_max A - lambda_max B| <= opnorm (A - B) <= frobenius (A - B), for all square matrices. For A symmetric, opnorm A = max (lambda_max A, lambda_max (- A)). | |||
| psd_ | 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. | ||
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). | |||
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. | |||
| spectral_ | A gap from the square: for B symmetric and positive semidefinite with k x^T B x <= |B x|^2 for every column x, k |x|^2 <= x^T B x for every x orthogonal to the kernel of B; in an eigenbasis, every eigenvalue is 0 or at least k. Used by target T4 of phase 12 for the spectral gap of the heat-bath dynamics. | ||
The Schur test for symmetric matrices: for B symmetric, rho >= 0 and sum_j |B_ij| <= rho for every row i, opnorm B <= rho. | |||
| nets.v | If N is an eps-net of the unit ball, then opnorm A <= max_{y in N} |A y| / (1 - eps), opnorm A <= max_{u, v in N} |u^T A v| / (1 - 2 eps), and for symmetric A, opnorm A <= max_{v in N} |v^T A v| / (1 - 2 eps). The bilinear bound also holds for nets of the unit sphere. | Spectral/ (opnorm_net_sphere); comparison/ in the library. The other three are used inside the library only | |
Every set in the ball of radius r of 'cV[R]_n has an eps-net of at most (2 e (1 + 2 r / eps))^n of its own points; for the unit ball and the unit sphere, r = 1. Proved by rounding to a grid of mesh eps / (2 sqrt n) and counting the grid points. | Spectral/ (unit_sphere_net); comparison/ in the library | ||
C(m, n) <= (e m / n)^n. There are C(n + k, n) lists of n natural numbers with sum at most k. | through net_exists | ||
| random_ | For S symmetric positive semidefinite and any square A, |<A, S>| <= opnorm (sym_part A) tr S, where sym_part A = (A + A^T) / 2 and <., .> is the Frobenius product. The unit ball of 'cV[R]_n has a 1/4-net V of at most (18 e)^n of its points, and opnorm (sym_part A) <= 2 max_{v in V} |v^T A v|. | ||
Maximal inequality: for x of law tuple_prod mu n, a family of N functions g_v, each centered and subexponential with constant L under every mu i, and |a_i| <= 1, E max_v |sum_i a_i g_v(x_i)| <= 8 L (sqrt (n Lam) + Lam) with Lam = 1 + ln (1 + 2 N). Proved with the moment generating function of each sum and e^y >= 1 + y. | |||
For x of law tuple_prod mu n and Y : T -> 'M[R]_m whose quadratic forms v^T Y v (|v| <= 1) are centered and subexponential with constant L under every mu k, there are measurable N a with opnorm (sym_part (sum_k a_k Y(x_k))) <= N a x and E N a <= 96 L (sqrt (n (m + 1)) + m + 1) for all weights with |a_k| <= 1. Unlike the matrix Bernstein inequality, the bound has no logarithmic factor. | |||
| von_ | 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 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'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. | |||
| nuclear.v | The nuclear norm, defined as the dual norm of opnorm for the Frobenius pairing: a norm with |<A, B>| <= opnorm B * nuclear A, frobenius A <= nuclear A <= sqrt n * frobenius A, nuclear (x x^T) = |x|^2, and for A = P^T diag(d) P with P orthogonal, nuclear A = sum_i |d_i|. | ||
Range duality (Koehler-Sohn Lemma 2.2): for W_1, ..., W_k in 'M[R]_n, if |<l, y>| <= M nuclear (sum_i l_i W_i) for every l, then y = (<W_i, D>)_i for some D with opnorm D <= M, symmetric when the W_i are. By the nearest point of y in the compact convex image of the operator-norm ball, without a general duality theorem. | |||
| psd_ | 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). | ||
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/. | |||
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. | |||
| condition_ | cond_cone C is the set of the symmetric Q with t I <= Q <= C t I for some t >= 0: the positive semidefinite matrices of condition number at most C, and 0. A symmetric Q is in it iff its eigenvalues lie in some [t, C t] with t >= 0; for C >= 0, iff Q is positive semidefinite with |y|^2 x^T Q x <= C |x|^2 y^T Q y for all x, y. In the coordinates of mxvec it is a closed convex cone, as the cone projection of convex/ asks. | ||
For C >= 1 and H symmetric, the squared Frobenius distance from H to cond_cone C is cond_dist C H, the infimum over t >= 0 of sum_i dist(lambda_i(H), [t, C t])^2: the lower bound by Hoffman-Wielandt, the upper bound by clipping the eigenvalues of H to [t, C t] (Tanaka and Nakata). The support function, the supremum of <H, Q> over the Q of the cone with |Q|_F <= 1, is the norm of the projection of H onto the cone, and its square is |H|_F^2 - cond_dist C H (Moreau's decomposition). Only the symmetric part of a matrix matters, the support function and cond_dist scale, and when the eigenvalues of H are at most T >= 0 the infimum over t may be taken over [0, T]. | |||
The trace slice {Q in cond_cone C : tr Q = n} is a closed convex base of the cone: for C > 0 and n >= 1 its matrices satisfy t I <= Q <= C t I for some t in [1/C, 1], have eigenvalues in [1/C, C] and n <= |Q|_F^2 <= C n, and every nonzero point of the cone has a positive multiple in it. | |||
| trace_ | trace_scale a S = S + a (tr S / n) I multiplies the component of S along the identity by 1 + a: trace_scale a (trace_scale b S) = trace_scale ((1 + a) (1 + b) - 1) S, it is self-adjoint for the Frobenius product, and tr (trace_scale a S) = (1 + a) tr S. (tr S)^2 / n <= |S|_F^2, so |S|_F^2 + (c / n) (tr S)^2 >= min(1, 1 + c) |S|_F^2 for every real c. trace_quad c H S = 2 <H, S> - |S|_F^2 - (c / n) (tr S)^2 has an exact second-order expansion at every X. | ||
For c > -1 and a nonempty convex set K of n x n matrices, closed in the coordinates of mxvec, trace_quad c H has a unique maximizer X = trace_argmax K c H on K. X is the only point of K with <H - X - (c / n) tr(X) I, S - X> <= 0 for every S in K, and trace_quad c H S + min(1, 1 + c) |S - X|_F^2 <= trace_quad c H X for S in K. Proved by the projection of convex/ after trace_scale (sqrt (1 + c) - 1), which turns the quadratic part into |.|_F^2. | |||
With the same hypotheses, |X(H) - X(H')|_F <= |H - H'|_F / min(1, 1 + c). If 0 is in K, then X(0) = 0 and |X(H)|_F <= |H|_F / min(1, 1 + c). If K is a cone, then <H, X> = |X|_F^2 + (c / n) (tr X)^2 = trace_quad c H X. If K is invariant under the conjugations S |-> P S P^T by orthogonal matrices, then X(Q H Q^T) = Q X(H) Q^T for every orthogonal Q. | |||
| effective_ | 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. | ||
| covering.v | Lemma 3.10 of Koehler and Sohn: if c0 d <= m, q <= C0 d with c0 > 0 and d > 0, the m x q matrices of nuclear norm at most gam d (written by duality: <A, B> <= gam d opnorm B for every B) are covered by exp ((96 C0 + 33) / c0^2) ^ (m q) translates of the product of the column balls of radius gam (the ball of colmax, the largest Euclidean norm of a column). In general, a set K with <A, B> <= r opnorm B on K has such a covering of size exp (48 (m + q) r / gam + 33). Proved by Sudakov's minoration and the dual Sudakov inequality instead of Urysohn's inequality. | ||
Small-ball probability of a random matrix with independent columns (the covering step of Lemma 3.14 of Koehler and Sohn): for distinct coordinates y_(g i j), i < n, j < q, of a tuple y of law tuple_prod mu N, and w_i in 'rV_m, if each column sum sum_i y_(g i j) w_i is within gam of any given vector with probability at most p, then the m x q matrix of these columns plus a fixed B lies in a measurable K with <A, C> <= r opnorm C on K (the nuclear-norm ball of radius r, for instance) with probability at most exp (48 (m + q) r / gam + 33) p^q. | |||
| tensor_ | Tensor packing (Theorem 4.1 of 'Pointwise convergence of fourfold ergodic averages for mixing transformations', family 154 of the OpenAI math collection): for rows x_1, ..., x_m and y_1, ..., y_m in the unit balls of 'rV[R]_n1 and 'rV[R]_n2, relations Gx and Gy on 'I_m with at most L successors at every vertex that contain every pair a != b with |<x_a, x_b>| > eta (respectively |<y_a, y_b>| > eta), Frobenius-orthonormal A_1, ..., A_r in 'M[R]_(n1, n2) with r <= d, 0 < eps <= 1, d >= 1 and 0 <= eta <= eps^2 / 10^4, at most 30000 (1 + L) / eps^2 exp (30000 sqrt d ln (2 + d) / eps^2) indices a have sum_k (x_a A_k y_a^T)^2 >= eps^2. Proved by cutting the spectra of sum_k A_k A_k^T and sum_k A_k^T A_k at sqrt d, Sudakov's minoration and gauss_mx_series_opnorm_log. | ||
Almost orthogonal families: if eta >= 0, <v_a, v_a> <= 1 and |<v_a, v_b>| <= eta for a != b outside a relation with at most L successors at every vertex, then |sum_(a in S) v_a|^2 <= (1 + L) s + eta s^2 with s = #|S|, so a set S with |sum_(a in S) v_a| >= rho s, rho >= 0 and rho^2 > eta has at most (1 + L) / (rho^2 - eta) elements. For such columns X_a in the unit ball of 'cV[R]_n, V in 'M[R]_(k, n) with V V^T = 1, eps > 0 and 0 <= eta <= eps^2 / 10^4, at most (2 e (1 + 80 / eps))^k 200 (1 + L) / eps^2 indices have |V X_a| > eps / 10. | |||
Bessel's inequality sum_k <Z, A_k>^2 <= <Z, Z> for a Frobenius-orthonormal family, so mxcoef A Z, the row of the <Z, A_k>, is a contraction. Every finite set I of indices has a subset J whose points v_b are pairwise at distance at least delta > 0 and such that every point of I is at distance less than delta from a point of J. A set covered by sets C_b, b in J, of at most B elements each has at most #|J| B elements. | |||
select_rows P S is the matrix of the rows of P indexed by S, with orthonormal rows when P is orthogonal; rowproj V = V^T V and rowperp V = 1 - V^T V are complementary orthogonal projections when V V^T = 1. For P orthogonal, t >= 0 and V = select_rows P [set u | t < e_u], the quadratic form of P^T diag(e) P on the range of rowperp V is at most t |z|^2. If this bound holds for sum_k A_k A_k^T and V1, the compressions B_k = rowperp V1 A_k rowperp V2 satisfy opnorm (sum_k B_k B_k^T) <= t and tr (sum_k B_k B_k^T) <= sum_k |A_k|_F^2. | |||
Sudakov's minoration for a Gaussian matrix series: if the coefficient vectors mxcoef B (x_i^T y_i) of l + 1 tensors of rows in the unit balls are pairwise at distance at least delta >= 0, then delta (sqrt (ln (l + 1)) / 2 - 2) <= sqrt 2 E opnorm (sum_k g_k B_k) for g of law gauss r; likewise with ln #|J| for a separated set J of indices. |