On this page
GaussianAnalysisrandom_matrix/
random_matrix/
The Gaussian orthogonal ensemble: the Schwinger-Dyson equation for its moments, the operator norm, Wigner's semicircle law, and the invariance of its law under orthogonal conjugation, with the diagonal of equivariant matrix functions; the restricted isometry of matrices with independent subexponential columns (Adamczak, Litvak, Pajor and Tomczak-Jaegermann) and the norms of sparse combinations of subgaussian vectors; the trace moments and the operator norm of Gaussian matrix series, and the sharp upper edge of the GOE (its largest eigenvalue has mean at most 2 and Gaussian tails above it).
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 studies random matrices over an arbitrary realType, mostly the Gaussian orthogonal ensemble. For a of law gauss (d * d), goe_mx a is the symmetric matrix W = (A + A^T) / sqrt (2 d) with A = vec_mx a; its entries W_ij, i <= j, are independent centered normals of variance 1 / d off the diagonal and 2 / d on it. As a function of the Gaussian vector a, W falls under the tools of gaussian/ and comparison/.
The GOE files give the Schwinger-Dyson equation, Wigner's semicircle law, the invariance under orthogonal conjugation, tails of the entries and the sharp upper edge. Two files leave the GOE: Gaussian matrix series sum_j g_j H_j, with bounds free of the dimension, and the restricted isometry of independent subexponential vectors (Adamczak, Litvak, Pajor and Tomczak-Jaegermann; ALPT below).
Reading order
goe.v: the GOE matrix, Gaussian integration by parts, the Schwinger-Dyson equation, operator-norm and trace-variance bounds.wigner.v: the convergence of the moments and Wigner's semicircle law.goe_rotation.v: invariance under orthogonal conjugation, applied to equivariant matrix functions.goe_entries.v: tails of the entries and of the row sums of squares.goe_edge.v: the sharp upper edge of the spectrum.matrix_series.v: Gaussian matrix series.restricted_isometry.v: restricted isometry, and norms of sparse combinations of independent vectors.
Core definitions
goe_mx(goe.v): (A + A^T) / sqrt (2 d) with A = vec_mx a.polyfun(goe.v): F is continuous with |F x| <= C (1 + |x|^k).mxpow_deriv(goe.v): sum_(r < k) W^r E W^(k-1-r), the derivative of M |-> M^k at W along E.goe_stat(wigner.v): (1 / d) sum_i f (spec W i).conj_equivariant,diag_var(goe_rotation.v): F (Q W Q^T) = Q F(W) Q^T for Q orthogonal and W symmetric; the empirical variance of the diagonal.sym_dilation(matrix_series.v): [[0, B], [B^T, 0]] for a rectangular B.gram_off,rip_const(restricted_isometry.v): sum_(i <> j) u_i v_j <x_i, x_j>; the supremum of |gram_off x u u| over the m-sparse u with |u| <= 1.
Main results
Below, a has law gauss (d * d) and W = goe_mx a.
Moments and the semicircle law.
goe_schwinger_dyson: E tr W^(k+1) = (k E tr W^(k-1) + sum_(r < k) E[tr W^r tr W^(k-1-r)]) / d.goe_moment_cvg: E tr W^k / d tends, as d grows, to the k-th moment of semicircle_prob 2.wigner: for f continuous on R and L-Lipschitz on [-3, 3] and eps > 0, P(|goe_stat f a - int f d(semicircle_prob 2)| >= eps) <= eps for every large d.wigner_uniformholds uniformly over t in [t0, t1] for continuous f_t that are L-Lipschitz in x and in t on [-3, 3], with the exceptional set inside a measurable event.
Edge and entries.
goe_lambda_max_mean,goe_lambda_maxN_mean: for d >= 1, E lambda_max W <= 2 and E lambda_max (- W) <= 2.goe_lambda_max_tail,goe_opnorm_edge_tail: for d >= 1 and t >= 0, P(lambda_max W >= 2 + t) <= exp (- d t^2 / 4) and P(opnorm W >= 2 + t) <= 2 exp (- d t^2 / 4).goe_mx_offdiag_tail,goe_mx_row_tail: for i != j and s >= 0, P(|W_ij| >= s) <= 2 exp (- d s^2 / 2); for u > 0, P(sum_(j != i) W_ij^2 >= 1 + u) <= exp (- d u^2 / (4 (1 + u))).
Rotation invariance.
goe_conj_integral: E F(Q^T W Q) = E F(W) for Q orthogonal and a |-> F (goe_mx a) measurable.goe_diag_var_tail: for F conj_equivariant, symmetric on symmetric matrices, with a |-> F (goe_mx a) measurable, C >= 0 and eps > 0, P(diag_var F(W) >= eps) <= 2 C / ((d + 2) eps) + P(|F(W)|_F^2 > C d).
Matrix series and sparse vectors.
gauss_mx_series_moment: for symmetric H_j, S = sum_j H_j^2, g of law gauss r and q >= 1, E tr (sum_j g_j H_j)^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S.gauss_mx_series_opnorm_log: for rectangular B_j and a real d >= 1 with opnorm (sum_j B_j B_j^T) and opnorm (sum_j B_j^T B_j) at most sqrt d and tr (sum_j B_j B_j^T) <= d, E opnorm (sum_j g_j B_j) <= 5 d^(1/4) sqrt (ln (2 + d)).restricted_isometry: let x_1, ..., x_N in 'rV_n have law tuple_prod mu N, every <x_i, y> with |y| = 1 centered and subexponential with constant psi > 0. For 1 <= m <= N, 0 < beta <= 1/2 and K >= 1, outside a measurable event of probability at most 2 (floor (log_4 m) + 2) exp (- K sqrt m (1 + ln (N / m))), rip_const m x <= 256 T^2 + 32 T C + 8 beta C^2, with T = 2100 K psi sqrt m (1 + ln (N / m) - ln beta) and C = max_i |x_i|.sparse_norm_subgaussian: if instead the <x_i, y> are centered and subgaussian with constant K > 0, then for 1 <= m <= N and s >= 0, outside a measurable event of probability at most 2 exp (- s), every m-sparse u has |sum_i u_i x_i| <= 8 K sqrt (m (1 + ln (N / m)) + 6 (m + n) + s) |u|.
How the proofs go
goe_schwinger_dyson: Gaussian integration by parts in each coordinate of a (gauss_ibp_polyfun) and the derivative of matrix powers (is_derive_mxpow).goe_moment_cvg: induction on k with the Schwinger-Dyson recursiongoe_tr_sd, whose covariance terms tend to 0 (goe_tr_cov_cvg);semicircle_catalan, fromsegner, gives the limit recursion for the semicircle moments.wigner: off the event opnorm W >= 3, Bernstein polynomials (weierstrass_lipschitz) handle the mean and Gaussian concentration the fluctuations.goe_lambda_max_mean: the Sudakov-Fernique inequality compares x_j^T W x_j, linear in a, with (2 / sqrt d) <g, x_j>, g of law gauss d, on finite families of unit vectors, and a net reaches the sphere; Gaussian concentration with the sharp constant gives the tails.goe_equiv_form: a Householder reflection replaces the Haar measure.gauss_mx_series_moment: integration by parts gives the recursiongauss_mx_series_trace_rec;sym_dilationhandles rectangular matrices.restricted_isometryfollows ALPT with value levels instead of sorted coordinates: conditional Bernstein bounds (cross_tail), decoupling (gram_off_decouple), nets and a union bound.
Connections
The directory requires gaussian/, comparison/, seven files of matrix/, fourier/, probability/, and for restricted_isometry.v the product laws, subgaussian variables and conditioning of probability/.
matrix/ uses matrix_series.v. applications/ uses matrix_series.v for T1, goe.v and goe_edge.v for T3, and goe.v, goe_rotation.v, goe_edge.v and goe_entries.v for T4. extension/ uses goe.v, wigner.v, goe_rotation.v and restricted_isometry.v; theories/ does not use the directory.
Files
| File | Title | Lines | Lemmas | Defs | Requires in this directory |
|---|---|---|---|---|---|
| goe.v | The Gaussian orthogonal ensemble | 1,256 | 71 | 6 | none |
| goe_edge.v | The upper edge of the Gaussian orthogonal ensemble | 400 | 22 | 2 | goe |
| goe_rotation.v | The rotation invariance of the GOE | 722 | 21 | 3 | goe |
| wigner.v | Wigner's semicircle law for the GOE | 1,129 | 33 | 3 | goe |
| restricted_isometry.v | Restricted isometry of matrices with independent psi_1 columns | 2,547 | 113 | 40 | none |
| matrix_series.v | Gaussian matrix series | 746 | 34 | 1 | goe |
| goe_entries.v | Tails of the entries of the GOE matrix | 528 | 21 | 1 | goe, goe_rotation |
Table of main results25 rows of the README
| File | Results | Statement |
|---|---|---|
| goe.v | The GOE matrix goe_mx a = (A + A^T) / sqrt (2 d), A = vec_mx a, for a of law gauss (d * d), and the Schwinger-Dyson equation E tr W^(k+1) = (k E tr W^(k-1) + \sum_(r < k) E[tr W^r tr W^(k-1-r)]) / d, by Gaussian integration by parts in each coordinate of a (for continuous functions of polynomial growth, polyfun) and the derivative of matrix powers (is_derive_mxpow). | |
E opnorm W <= 2 sqrt 2 for d >= 1 (from Gordon's bound gauss_opnorm_mean), E exp (s opnorm W) <= exp (2 sqrt 2 s + s^2 / d) for s >= 0, and P(opnorm W >= c) tends to 0 for every c > 2 sqrt 2. | ||
Var (tr W^k / d) tends to 0, with the bound 2 L^2 + 8 (2k)! exp (2 sqrt 2 (2u + 1) + (2u + 1)^2 / d - 6u) for every u >= 0, L = sqrt 2 k 3^(k-1) / d: the statistic of the eigenvalues clipped to [-3, 3] is L-Lipschitz (Hoffman-Wielandt) and obeys the Gaussian Poincare inequality. |Cov (X, Y)| <= (Var X + Var Y) / 2. | ||
| goe_ | For d >= 1, a of law gauss (d * d) and the GOE matrix W = goe_mx a: E lambda_max W <= 2 and E lambda_max (- W) <= 2. For every finite family of unit columns x_j, E max_j x_j^T W x_j <= 2, by the Sudakov-Fernique inequality against (2 / sqrt d) <g, x_j> for g of law gauss d, whose increments have larger variances; a net of the unit sphere passes to lambda_max. A Rocq formalization of the credited argument of family 227 of the OpenAI math collection (see the header). | |
For d >= 1 and t >= 0: P(lambda_max W >= 2 + t) <= exp (- d t^2 / 4), the same for - W, and P(opnorm W >= 2 + t) <= 2 exp (- d t^2 / 4). The maps a |-> lambda_max W and a |-> lambda_max (- W) are sqrt (2 / d)-Lipschitz for every d, hence measurable and integrable, and Gaussian concentration with the sharp constant gives the tails. | ||
For a square matrix A of size n > 0 and unit columns x_j such that every unit column lies within eps of some x_j: lambda_max A <= max_j x_j^T A x_j + 2 eps opnorm A. | ||
| goe_ | For a of law gauss (d * d) and the GOE matrix W = goe_mx a, every entry is a linear form of a: W_ij = <a, goe_coef i j>. For s >= 0: P(|W_ii| >= s) <= 2 exp (- d s^2 / 4), and P(|W_ij| >= s) <= 2 exp (- d s^2 / 2) if i != j. For u > 0 and every i: P(sum_(j != i) W_ij^2 >= 1 + u) <= exp (- d u^2 / (4 (1 + u))), since d sum_(j != i) W_ij^2 has the law of a chi-square with d - 1 degrees of freedom. A Rocq formalization of the credited argument of a proposition of family 227 of the OpenAI math collection (see the header). | |
Union bounds over the entries and the rows: for s >= 0 and u > 0, P(max_i |W_ii| >= s) <= 2 d exp (- d s^2 / 4), P(max_(i != j) |W_ij| >= s) <= 2 d^2 exp (- d s^2 / 2) and P(max_i sum_(j != i) W_ij^2 >= 1 + u) <= d exp (- d u^2 / (4 (1 + u))). These events, and {opnorm W >= c} for every real c, are measurable. | ||
For a square matrix A and b >= 0 with |A_ii| <= b for every i: opnorm (A - diag A) <= opnorm A + b, because opnorm (diag_mx v) <= b when every |v_i| <= b. For a measure mu, a finite index type and measurable sets F i: mu (\bigcup_i F i) <= \sum_i mu (F i). For c > 0, x >= 1 and k <= 2: x^k exp (- x c) <= 6 / (c^3 x). | ||
| wigner.v | E tr W^k / d tends to \int x^k d(semicircle_prob 2) for every k, by induction from the Schwinger-Dyson equation, whose covariance terms vanish in the limit; the semicircle moments satisfy the same recursion (Segner's recurrence for the Catalan numbers, proved from their ratio recurrence). | |
Wigner's semicircle law: for f continuous and Lipschitz on [-3, 3] and eps > 0, P(|(1 / d) \sum_i f (spec W 0 i) - \int f d(semicircle_prob 2)| >= eps) <= eps for every large d. | ||
Wigner's law uniformly over a family f_t, t in [t0, t1], of continuous functions that are L-Lipschitz on [-3, 3] and L-Lipschitz in t there: for every eps > 0 and every large d, the event that |(1 / d) \sum_i f_t (spec W 0 i) - \int f_t d(semicircle_prob 2)| >= eps for some t lies in a measurable event of probability at most eps. | ||
Under the hypotheses of wigner_uniform, with t0 <= t1: the infimum over t in [t0, t1] of goe_stat (f t) a converges in probability to the infimum over t of \int f_t d(semicircle_prob 2). For every eps > 0 and every large d, the samples where the two infima differ by at least eps lie in a measurable set of Gaussian probability at most eps. No minimum needs to be attained. | ||
Weierstrass's approximation theorem for Lipschitz functions: if f is L-Lipschitz on [a, b], then for every eps > 0 some polynomial p satisfies |p.[x] - f x| <= eps on [a, b]. On [0, 1] the Bernstein polynomial of f of degree n >= 1 is within L / (2 sqrt n) of f. | ||
| goe_ | The law of the GOE matrix W is invariant under W |-> Q^T W Q for every orthogonal Q. For F equivariant (F (Q W Q^T) = Q F(W) Q^T for every orthogonal Q and symmetric W) and every unit row vector u, u F(W) u^T has the law of F(W)_00: a Householder reflection maps the first basis vector to u. | |
Lemma 5.13 of Koehler and Sohn without the Haar measure. For F equivariant with F(W) symmetric and E F(W)_ij^2 finite, E[diag_var F(W)] = 2 / (n + 2) E[|F(W)|_F^2 / n - (tr F(W) / n)^2], where diag_var A is the empirical variance of the diagonal of A. Without moment assumptions, P(diag_var F(W) >= eps) <= 2 C / ((n + 2) eps) + P(|F(W)|_F^2 > C n) for every C >= 0 and eps > 0. | ||
| restricted_ | Theorem 5.1 of Adamczak, Litvak, Pajor and Tomczak-Jaegermann at r = 1, with explicit constants. Let x_1, ..., x_N in 'rV[R]_n be independent (tuple_prod mu N), with every linear form <x_i, y>, |y| = 1, centered and subexponential with constant psi. For 1 <= m <= N, 0 < beta <= 1/2 and K >= 1, outside a measurable event of probability at most 2 (log_4 m + 2) exp (- K sqrt m (1 + ln (N / m))), every m-sparse u of norm at most one satisfies ||sum_i u_i x_i|^2 - sum_i u_i^2 |x_i|^2| <= 256 T^2 + 32 T C + 8 beta C^2, where T = 2100 K psi sqrt m (1 + ln (N / m) - ln beta) and C = max_i |x_i|. | |
With B^2 = rip_const m x (the supremum above) and C = max_i |x_i|, for all m-sparse u and v: |gram_off x u u| <= B^2 |u|^2, |sum_i u_i x_i| <= sqrt (B^2 + C^2) |u| and |gram_off x u v| <= (B^2 + 2 C^2) |u| |v|, where gram_off x u v = sum_(i <> j) u_i v_j <x_i, x_j>. | ||
For a and b in 'rV[R]_N with disjoint supports, |a| <= 1 and |a_i| <= al for all i, and t > 0: P(|<sum_i a_i x_i, sum_j b_j x_j>| > t |sum_j b_j x_j|) <= 2 exp (- min (t^2 / (64 psi^2), t / (4 al psi))), by Bernstein's inequality conditionally on the vectors in the support of b. | ||
Decoupling: if y is supported in F and |<sum_(i in E) y_i x_i, sum_(j in F \ E) y_j x_j>| <= c for every E included in F, then |gram_off x y y| <= 4 c. Nets: the vectors supported in F with norm at most one and coordinates at most al have an eps-net of at most (2 e (1 + 2 / eps))^|F| points. Counting: there are at most (e N / s)^s subsets of {1, ..., N} with at most s elements, for 1 <= s <= N. | ||
The restricted isometry constant: for every m-sparse u, ||sum_i u_i x_i|^2 - |u|^2| <= (rip_const m x + max_i ||x_i|^2 - 1|) |u|^2. Blocks: if |sum_i u_i x_i| <= L |u| for every m-sparse u, then |sum_i u_i x_i| <= L sqrt (N / m + 1) |u| for every u (deterministic). | ||
Norms of sparse combinations of independent subgaussian vectors: if x_1, ..., x_N in 'rV[R]_n are independent (tuple_prod mu N) with every linear form <x_i, y>, |y| = 1, centered and subgaussian with constant K, then for 1 <= m <= N and s >= 0, outside a measurable event of probability at most 2 exp (- s), every m-sparse u satisfies |sum_i u_i x_i| <= 8 K sqrt (m (1 + ln (N / m)) + 6 (m + n) + s) |u| (Vershynin's Theorem 4.4.5 with a union bound over the supports). For unit a and y, P(|<sum_i a_i x_i, y>| >= t) <= 2 exp (- t^2 / (16 K^2)). | ||
| matrix_ | Gaussian matrix series. For symmetric H_1, ..., H_r in 'M[R]_n, S = \sum_j H_j^2 and g of law gauss r, the series X = \sum_j g_j H_j satisfies E tr X^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S for every q >= 1, with no dimension in the bound (an integral in the extended reals). It follows from E tr X^2 = tr S, which needs no symmetry, and the recursion E tr X^(2q+2) <= (2q + 1) opnorm S E tr X^(2q). The recursion comes from Gaussian integration by parts in each coordinate, E tr X^(k+1) = \sum_j E tr (H_j D_j) with D_j the derivative of X^k along H_j. Lemma 4.2 of the fourfold ergodic paper of family 154 of the OpenAI math collection (revision 1581d4cbd). | |
For B_1, ..., B_r in 'M[R]_(m, p) and g of law gauss r, with sigma^2 = max (opnorm (\sum_j B_j B_j^T), opnorm (\sum_j B_j^T B_j)) and tau = 2 tr (\sum_j B_j B_j^T): E opnorm (\sum_j g_j B_j)^(2q) <= (2q - 1)!! sigma^(2(q-1)) tau and E opnorm (\sum_j g_j B_j) <= ((2q - 1)!! sigma^(2(q-1)) tau)^(1/(2q)) for every q >= 1, through the symmetric dilation sym_dilation B_j = [[0, B_j], [B_j^T, 0]]. If the two operator norms are at most sqrt d and tr (\sum_j B_j B_j^T) <= d for a real d >= 1, then E opnorm (\sum_j g_j B_j) <= 5 d^(1/4) sqrt (ln (2 + d)). No dimension of the matrices enters. | ||
|tr (K A^a K A^b)| <= tr (K^2 A^(a+b)) for symmetric K and A and a + b even. tr (S T) <= opnorm S tr T for T positive semidefinite (psdmx T) and any square S. For a probability P, a measurable f >= 0 and k >= 0, E f <= (E f^(k+1))^(1/(k+1)), the expectations being integrals in the extended reals, and E f^(k+1) <= t^(k+1) with t > 0 gives E f <= t. |