On this page
Main results
The tables of main results of library/README.md and applications/README.md: each row names the results of a file and states them informally, with their hypotheses. The names link to the declarations, whose pages give the statements that Rocq checks. The rows are grouped by directory, in the order of the layout table, and keep the README order inside each directory.
gaussian/39 rows
| File | Results | Statement | Used by theories/ |
|---|---|---|---|
| measurable_ | A map into 'M[T]_(m, n) is measurable if and only if each of its entries is. Matrices carry the sigma-algebra generated by their entries. | Gaussian/ | |
| Two measures on matrices (or row vectors) that agree on the boxes with measurable sides, the first of them finite, agree on every measurable set. | through gauss_unique | ||
A continuous real function of a real matrix is measurable: the open sets of 'M[R]_(m, n) are measurable. | Gaussian/ | ||
For the norm of a real matrix: every entry is bounded by the norm, |A B| <= n |A| |B| when A has n columns, |col_mx P Q| <= |P| + |Q|, and permuting the columns does not increase the norm. | Gaussian/ | ||
| A map into real matrices is continuous if each of its entries is, and the matrix product is continuous in each factor. | |||
| normal_ | Integrating against normal_prob m s is integrating against Lebesgue measure with the density normal_pdf m s, for nonnegative or integrable functions. | ||
Every power |x|^k, hence every measurable function bounded by C (1 + |x|^k), is integrable against the standard normal law. | |||
| gauss.v | gauss n, the standard Gaussian measure on 'rV[R]_n: the law of n independent standard normal coordinates, a probability. | Gaussian/, Gaussian/, Gaussian/, Gaussian/, Projected/ | |
gauss n gives the box with sides A i the measure \prod_i normal_prob 0 1 (A i), and it is the only measure on 'rV[R]_n that does. | Gaussian/ | ||
Fubini for the first coordinate: the integral against gauss n.+1 is the iterated integral against normal_prob 0 1 and gauss n, and integrability against gauss n.+1 is integrability against the product of the two. | Gaussian/, for Gaussian/ | ||
Independent blocks: the image of gauss n \x gauss m under (x, y) |-> row_mx x y is gauss (n + m). | |||
gauss n, and the integral of every integrable function against it, are invariant under permutations of the coordinates. | Gaussian/, for Gaussian/ | ||
Marginals of the blocks: if x has law gauss (n + m), then lsubmx x has law gauss n and rsubmx x has law gauss m. | |||
If nu is the image of the measure mu under a measurable g, then \int[mu] f (g x) = \int[nu] f y for every nu-integrable f. | |||
Each coordinate of a vector of law gauss n has law normal_prob 0 1. | |||
Independent coordinates: the integral of \prod_i f i (x 0 i) against gauss n is \prod_i of the integrals of f i against normal_prob 0 1, for nonnegative measurable f i. | |||
Every measurable function bounded by C (1 + |x|^k) is integrable against gauss n. The constant of such a bound is nonnegative, and multiplying the function by a coordinate raises k by one and doubles C. | Gaussian/ | ||
| gauss_ | Stein's identity: E[X f(X)] = E[f'(X)] for X of law normal_prob 0 1 and f differentiable with a continuous derivative, f and f' of polynomial growth. | ||
Gaussian integration by parts: E[x_i F(x)] = E[d_i F(x)] for x of law gauss n, F continuous with a continuous partial derivative d_i F (along delta_mx 0 i), both of polynomial growth. | Gaussian/, for Gaussian/ | ||
The same identity when F and d_i F are only measurable and d_i F is continuous along the lines parallel to the i-th axis. | |||
If a measurable function on 'rV[R]_n has at every point x a derivative dF x along a fixed vector v, then dF is measurable. | |||
Gaussian integration by parts of order two: E[(x_i^2 - 1) F(x)] = E[d_i d_i F(x)] for x of law gauss n, F measurable, d_i d_i F continuous, and F, d_i F and d_i d_i F of polynomial growth; d_i F need not be continuous. | Gaussian/, for Gaussian/ | ||
If F i increases to U and g is integrable on U, the integrals of g over F i converge to its integral over U. | |||
| gauss_ | Moments of the standard normal law: E[X^(k+2)] = (k + 1) E[X^k], so the odd moments vanish and E[X^(2k)] = 1 * 3 * ... * (2k - 1). | ||
A vector x of law gauss n has mean 0 and covariance the identity, and x *m A has covariance A^T *m A. | |||
| partial_ | A function on 'rV[R]_n whose partial derivatives exist everywhere and are continuous is differentiable, with differential v |-> \sum_j v_j d_j F x. | ||
| parameter_ | Sequential criterion for a limit at a point x0 of a pseudometric space: f x tends to l as x tends to x0 as soon as f (u n) tends to l for every sequence u that tends to x0. | ||
Continuity of a parameter integral at a point x0 of a pseudometric space: if f x y is continuous in x at x0 for every y in B, and bounded by an integrable g y for x near x0, then x |-> \int_B f x y dmu(y) is continuous at x0. MathComp-Analysis states this for a real parameter in an open interval. | Gaussian/, for Gaussian/ | ||
| gauss_ | Integration by parts through a linear map: E[x_i d_j F (x *m M)] = \sum_l M_(i, l) E[d_l d_j F (x *m M)]. | ||
Gaussian interpolation: let x have law gauss n, let the path of matrices M t be differentiable on an open interval with derivative M' t, with |M t| <= K and |M' t| <= K on the interval, and let F be of class C^2 with F and its partial derivatives of order 1 and 2 all bounded by one C (1 + |z|^p). Then at every t of the interval the derivative of t |-> E[F (x *m M t)] is \sum_(j, l) ((M' t)^T M t)_(j, l) E[d_l d_j F (x *m M t)]. | |||
Kahane's comparison inequality, for F of class C^2 with the same growth hypothesis: if \sum_(j, l) (A^T A - B^T B)_(j, l) d_l d_j F <= 0 everywhere, then E[F (x *m A)] <= E[F (y *m B)] for x of law gauss n and y of law gauss m. | |||
The same comparison for F given by its partial derivatives of order 1 and 2, those of order 2 continuous. | |||
| lebesgue_ | lebesgue_rV n, Lebesgue measure on 'rV[R]_n, a sigma-finite measure built as gauss n is. A box with measurable sides A i has measure \prod_i lebesgue_measure (A i), and every measure on 'rV[R]_n that gives the boxes these values agrees with lebesgue_rV n on all measurable sets. | ||
Fubini: the integral against lebesgue_rV n.+1 is the iterated integral over the first coordinate and the others, and the integral against lebesgue_rV (n + m) is the iterated integral over the blocks x and y of row_mx x y, for nonnegative measurable or for integrable functions. The integral of \prod_i f i (x_i) is \prod_i of the integrals of the f i against Lebesgue measure. | |||
lebesgue_rV n is invariant under translations and permutations of the coordinates, and the preimage of X under x |-> a x, a != 0, has measure |a|^-n times that of X; the same for integrals (\int f (a x) dx = |a|^-n \int f), for nonnegative measurable and for integrable f. | |||
If the preimage of every box under a measurable phi has c > 0 times the measure of the box, then so has the preimage of every measurable set, and \int f (phi x) dx = c \int f. | |||
gauss n has the density gauss_pdf x = (2 pi)^(-n/2) exp (- mxdot x x / 2) with respect to lebesgue_rV n: E[f(x)] = \int f gauss_pdf, and \int f = E[f(x) / gauss_pdf x]. | |||
\int exp (- mxdot (x - z) (x - z) / (2 s^2)) dx = (sqrt (2 pi) s)^n over 'rV[R]_n, for s > 0. | |||
The closed Euclidean ball [set x | frobenius (x - z) <= r] of 'rV[R]_n, r > 0, has measure at most (sqrt (2 pi e / n) r)^n. |
comparison/68 rows
| File | Results | Statement | Used by theories/ |
|---|---|---|---|
| normal_ | The moment generating function of normal_prob m s, for s != 0, is t |-> expR (t m + t^2 s^2 / 2). | ||
For X of law normal_prob m s and u >= 0, P(X >= m + u) and P(X <= m - u) are at most expR (- u^2 / (2 s^2)), and P(|X - m| >= u) is at most twice that. | |||
Chernoff's bound: P(u <= f) <= E[expR (t (f - u))] for every measure, measurable f and t >= 0. | |||
| chi_ | For X of law normal_prob 0 s and 2 t s^2 < 1, E[expR (t X^2)] = 1 / sqrt (1 - 2 t s^2); for the standard law, E[expR (t (X^2 - 1))] = expR (- t) / sqrt (1 - 2 t). | Gaussian/, for Gaussian/ | |
- ln (1 - u) - u <= u^2 / (2 (1 - |u|)) for |u| < 1; hence E[expR (t (X^2 - 1))] <= expR (t^2 / (1 - 2 |t|)) for the standard normal law and |2 t| < 1. | |||
For x of law gauss n and weights a with |a_i| <= L, Q = sum_i a_i (x_i^2 - 1) satisfies E[expR (t Q)] <= expR (t^2 |a|^2 / (1 - 2 |t| L)) when 2 |t| L < 1, and P(|Q| >= u) <= 2 expR (- u^2 / (4 (|a|^2 + L u))) for u > 0. | Gaussian/ | ||
| normal_ | Under x |-> a x + b with a != 0, Lebesgue measure on the line is multiplied by |a|^-1. | ||
The image of normal_prob m s under x |-> a x + b, a != 0, is normal_prob (a m + b) (a s). | |||
If X and Y are independent, of laws normal_prob m1 s1 and normal_prob m2 s2, and b != 0, then a X + b Y has law normal_prob (a m1 + b m2) (sqrt (a^2 s1^2 + b^2 s2^2)). | |||
| gauss_ | For x of law gauss n and a != 0, the linear form mxdot x a has law normal_prob 0 (frobenius a), the normal law with variance |a|^2. | ||
E[expR (t <x, a>)] = expR (t^2 |a|^2 / 2), and P(|<x, a>| >= u) <= 2 expR (- u^2 / (2 |a|^2)). | Gaussian/ | ||
| gauss_ | Lebesgue measure on the plane is invariant under rotations (each is a product of three shears). | ||
| The standard Gaussian measure on the plane is invariant under rotations. | |||
For independent x, y of law gauss n and c^2 + s^2 = 1, the pair (c x - s y, s x + c y) has the law of (x, y); in particular c x + s y has law gauss n. | |||
| gauss_ | Cameron-Martin formula: for x of law gauss n, E[f (x + h)] = E[f x expR (<h, x> - |h|^2 / 2)]. | ||
| gauss_ | For G bounded and L-Lipschitz (Euclidean norm) and eps > 0, the Gaussian smoothing x |-> E[G (x + eps y)] is differentiable, with partial derivatives E[G (x + eps y) y_j] / eps, continuous, of gradient norm at most L, and within L eps E[|y|] of G. | ||
The gradient of a function of class C^1 that is L-Lipschitz for the Euclidean norm has Euclidean norm at most L. | |||
| gauss_ | For x of law gauss n, F bounded of class C^1 with gradient norm at most L, and t >= 0: E[F expR (t F)] <= (E[F] + t L^2) E[expR (t F)]. | ||
Gaussian concentration (Tsirelson, Ibragimov, Sudakov): if F is L-Lipschitz for the Euclidean norm, then E[expR (t (F x - E F))] <= expR (t^2 L^2 / 2) for every real t. | Gaussian/ | ||
For such F and u >= 0, P(F x >= E F + u) and P(F x <= E F - u) are at most expR (- u^2 / (2 L^2)), and P(|F x - E F| >= u) is at most twice that. | |||
Gaussian Poincaré inequality for Lipschitz functions: if F is L-Lipschitz for the Euclidean norm and x has law gauss n, then E[(F x - E F)^2] <= L^2. | Gaussian/ | ||
2 + x^2 <= expR x + expR (- x) for every real x, and 2 y <= expR y - expR (- y) for y >= 0. | |||
For (x, y) of law gauss n \x gauss n: the marginals are gauss n, the components are independent, and E[y_j H(x, y)] = E[d_(y_j) H(x, y)]. | |||
| slepian.v | Sudakov-Fernique inequality: for x of law gauss n and y of law gauss m, if each increment (x A)_j - (x A)_l has variance at most that of (y B)_j - (y B)_l, then E[max_j (x A)_j] <= E[max_j (y B)_j]. | ||
Slepian's inequality for expected maxima: if x A and y B have the same variances and each covariance of x A is at least that of y B, then E[max_j (x A)_j] <= E[max_j (y B)_j]. | |||
The log-sum-exp function lse b z = ln (\sum_j expR (b z_j)) / b, b > 0, satisfies max_j z_j <= lse b z <= max_j z_j + ln (k + 1) / b. Its Hessian paired with a matrix M is b / 2 \sum_(j, l) p_j p_l (M_jj + M_ll - 2 M_jl), with p the softmax weights. | |||
| gordon.v | Gordon's min-max inequality: for x of law gauss n, y of law gauss m and the Gaussian matrices X = vec_mx (x A), Y = vec_mx (y B), if each increment X_ut - X_us within a row has variance at most that of Y_ut - Y_us, and each increment X_ut - X_vs across distinct rows has variance at least that of Y_ut - Y_vs, then E[min_u max_t X_ut] <= E[min_u max_t Y_ut]. | ||
Gordon's inequality with equal variances: if the covariances of X are at least those of Y within each row and at most those of Y across rows, then E[min_u max_t X_ut] <= E[min_u max_t Y_ut]. | |||
If H has zero row and column sums, \sum_(i, j) M_ij H_ij = - 1/2 \sum_(i, j) H_ij (M_ii + M_jj - 2 M_ij). The soft min-max smm b z = - ln (\sum_u (\sum_t expR (b z_ut))^-1) / b is within ln (p + 1) / b below and ln (q + 1) / b above min_u max_t z_ut, and its Hessian is nonpositive within rows and nonnegative across rows. | |||
mxvec_index i j is the row-major position i * n + j, and a sum over 'I_(m * n) is the double sum over the pairs (i, j). | Gordon/ | ||
| escape.v | Gordon's escape through a mesh: let G = vec_mx a be an N x M matrix of independent standard normal entries (a of law gauss (N * M)), N > 0, and T a nonempty set of unit vectors of 'cV[R]_M. Then E[inf_(x in T) |G x|] >= E[|g|] - w(T), where w(T) = E[sup_(x in T) <h, x>] is the Gaussian width of T, and inf_(x in T) |G x| <= E[|g|] - w(T) - u has probability at most expR (- u^2 / 2). | Gordon/ | |
For such G with N, M > 0: E[opnorm G] <= E[|g|] + E[|h|] <= sqrt N + sqrt M, and opnorm G >= E[|g|] + E[|h|] + u has probability at most expR (- u^2 / 2). | |||
E[inf_(|x| = 1) |G x|] >= E[|g|] - E[|h|]: the Gaussian width of the unit sphere is E[|h|]. | |||
E[|g|] <= sqrt n for g of law gauss n, and gauss n is invariant under x |-> - x. | Gaussian/ | ||
Gordon's comparison for the min-max of the bilinear form: for nonempty sets T and Y of unit vectors of 'cV[R]_M and 'cV[R]_N, E[inf_(x in T) sup_(y in Y) <y, G x>] >= E[sup_(y in Y) <g, y>] - w(T). For an orthogonal projection P != 0 of 'cV[R]_N and Y the unit vectors of its range, E[inf_(x in T) |P G x|] >= E[|g P|] - w(T), with the tail expR (- u^2 / 2) below the mean; E[|g A|^2] = |A|^2 (gauss_sqr_mulmx) and, by the Poincare inequality, E[|g P|] >= sqrt (tr P - 1). So for M > 0, inf_(|x| = 1) |P G x| <= sqrt (tr P - 1) - sqrt M - u has probability at most expR (- u^2 / 2). | |||
For finite families of unit vectors xs u and ys t, Gordon's and the Sudakov-Fernique comparisons of the processes ys_t^T G xs_u and <g, ys_t> + <h, xs_u>; auxT_bilT_minmax is Gordon's comparison with the minimum over the left factor, zs_u^T G vs_t against <g, zs_u> + <h, vs_t>. | Gordon/ | ||
| gauss_ | Two descriptions of the law of an n x m matrix vec_mx a of independent standard normal entries (a of law gauss (n * m)): the matrix tuple_mx t of n independent rows of law gauss m has this law, tuple_prod (fun=> gauss m) n (tuple_mx @^-1` X) = gauss (n * m) [set a | X (vec_mx a)], and so has the transpose of an m x n such matrix, gauss (n * m) [set a | X (vec_mx a)^T] = gauss (m * n) [set b | X (vec_mx b)]. Both by gauss_unique on boxes. | ||
| cgmt.v | The convex Gaussian min-max theorem in mean form (Theorem 5.3 of Koehler and Sohn; Thrampoulidis, Oymak and Hassibi, Theorem 3): let A = vec_mx a be an N x M matrix of independent standard normal entries, z = (g, h) of law gauss (N + M), and K a nonempty set of 'cV[R]_M with |x| <= rho on K; let Phi(K) = inf_(x in K) |A x| (escape_inf) and phi(K) = inf_(x in K) (|g| |x| - <h, x>)_+ (cgmt_aux). Then E Phi(K) >= E phi(K) - rho for N > 0, and E Phi(K) <= E phi(K) + rho for K closed and convex. | ||
Phi(K) is rho-Lipschitz in a and phi(K) is sqrt 2 rho-Lipschitz in z, so they are at least u away from their means with probability at most 2 exp (- u^2 / (2 rho^2)) and 2 exp (- u^2 / (4 rho^2)). For N > 0 and K closed and convex, Phi(K) is at least rho + u away from E phi(K) with probability at most 2 exp (- u^2 / (2 rho^2)). | |||
Gordon's comparison of |x| <g, y> + |y| <h, x> with y^T A x + gamma |x| |y|, gamma an independent standard normal, for finite families and, by nets, as E inf_(s in S) sup_(t in T) inequalities for bounded index sets; the minimax exchange inf_(x in K) |A x| <= sup_(|y| <= 1) inf_(x in K) <y, A x> for K closed, bounded and convex; closed bounded sets of column vectors are compact. | |||
Phi(K) and phi(K) are measurable functions of the Gaussian entries, so that their laws are defined. For a set K of row vectors, the theorems apply to the set tr_set K of the transposes, with Phi = inf_(x in K) |A x^T| and phi = inf_(x in K) (|g| |x| - <h, x>)_+; tr_set K is nonempty, bounded, closed or convex with K. | |||
If phi(K) vanishes with probability more than 1/2, then E phi(K) <= 2 rho sqrt (ln 4) (concentration), and Phi(K) >= rho (1 + 2 sqrt (ln 4)) + u has probability at most 2 exp (- u^2 / (2 rho^2)): the approximate solutions of A x = 0 on K that the CGMT gives when the auxiliary problem has the value 0. | |||
| cone_ | For a set K of 'cV[R]_M containing 0, sigma_K(h) = sup_(x in K, |x| <= 1) <h, x> lies in [0, |h|], is 1-Lipschitz in h, and is attained when K is closed (compactness). For a cone K (a x in K for x in K and a >= 0), <h, x> <= |x| sigma_K(h) on K. For a closed convex cone K of row vectors, sigma_(tr_set K)(h) = |proj K h| (cone_proj_support). | ||
The auxiliary value of the CGMT on a set B that contains a positive multiple of every nonzero point of a cone K: for K closed, cgmt_aux B g h = 0 when 0 < sigma_K(h) and |g| <= sigma_K(h), in particular when 0 < |g| <= sigma_K(h); for B nonempty and in K and r <= |x| on B, cgmt_aux B g h >= r (|g| - sigma_K(h))_+. The tr versions state the same for a closed convex cone and a set of row vectors, with |proj K h| in place of sigma_K(h). | |||
The CGMT on cones, for A = vec_mx a an N x M matrix of independent standard normal entries (N > 0), z = (g, h) of law gauss (N + M) and B as above, nonempty with |x| <= rho on B. If rho > 0, K is closed, B is closed and convex and P(|g| < sigma_K(h)) > 1/2, then inf_(x in B) |A x| >= rho (1 + 2 sqrt (ln 4)) + u has probability at most 2 exp (- u^2 / (2 rho^2)): the kernel of A meets K approximately. If B is in K and r <= |x| on B, then inf_(x in B) |A x| <= r E (|g| - sigma_K(h))_+ - rho - u has probability at most 2 exp (- u^2 / (2 rho^2)): the kernel stays away from B. | |||
| sudakov.v | Sudakov's minoration: if xs i, i < k + 1, are pairwise at distance at least eps in 'rV[R]_n, then eps (sqrt (ln (k + 1)) / 2 - 2) <= sqrt 2 E max_i <g, xs i> for g of law gauss n; the maximum of n independent standard normal variables has mean at least sqrt (ln n) / 2 - 2. | ||
The dual Sudakov inequality of Pajor and Tomczak-Jaegermann (Talagrand's proof): for a measurable seminorm nrm with E nrm(g) <= L, the points of the Euclidean ball of radius r that are pairwise more than eps apart for nrm are at most 2 exp (8 r^2 L^2 / eps^2). gauss n (h + A) >= exp (- |h|^2 / 2) gauss n A for A measurable and symmetric. A set whose eps-separated lists have at most M points has an eps-net of at most M of its points. | |||
| gauss_ | The law of a centered Gaussian vector depends only on its covariance: for x of law gauss n and y of law gauss m, if A^T *m A = B^T *m B, then P(x *m A \in X) = P(y *m B \in X) for every measurable set X of 'rV[R]_k, and E[f (x *m A)] = E[f (y *m B)] for every measurable f. | Gaussian/ | |
If the columns of A are orthonormal, x *m A has law gauss k; in particular gauss n is invariant under every orthogonal matrix. Forms with integrals. | Projected/ | ||
Gaussian vectors x *m A and y *m B with A^T *m A = B^T *m B give the same expectation to every test of class C^2 with polynomially bounded derivatives (Kahane's inequality in both directions), and to every bounded Lipschitz function. | |||
A finite measure on 'rV[R]_k is determined by the integrals of the Lipschitz functions with values in [0, 1]; the sets {Phi > 0}, for Phi nonnegative and Lipschitz, generate the Borel sets. | |||
For G bounded and Lipschitz, the partial derivatives of gauss_smooth eps G are bounded and Lipschitz, and smoothing them again equals differentiating the double smoothing. | |||
| ornstein_ | The Mehler transform mehler r f x = E[f (r x + sqrt (1 - r^2) Z)], Z of law normal_prob 0 1, and the Ornstein-Uhlenbeck semigroup ou t f = mehler (expR (- t)) f (Mehler's formula). mehler 1 f = f and mehler 0 f is the mean of f. | ||
For f bounded and measurable: the bounds of f hold for mehler r f; for |r| < 1 the standard normal law is invariant, E[mehler r f] = E[f], and mehler r is a contraction of L^1 of that law. | |||
For |r| < 1 the law of r x + sqrt (1 - r^2) Z has the density mehler_kernel r x, an explicit exponential of a quadratic polynomial, with respect to normal_prob 0 1. | |||
Differentiation under the integral against normal_prob 0 1, with a bounded measurable factor, for a kernel and its derivative in the parameter dominated by C expR (c |y|) on an open interval. | |||
For f bounded and measurable and |r| < 1, mehler r f has derivatives of order 1, 2 and 3 in x and a derivative in r, given by integrals against Hermite polynomials (mehler_d1, mehler_d2, mehler_d3, mehler_dr): for instance (mehler r f)' x = r / b E[f (r x + b Z) Z] with b = sqrt (1 - r^2). Generator identity: r d/dr mehler r f = x (mehler r f)' - (mehler r f)''. | |||
For t > 0, the first two derivatives of ou t f in x, and d/dt ou t f x = (ou t f)'' x - x (ou t f)' x. | |||
For |f| <= K and |r| < 1: |(mehler r f)'| <= |r| / b K E|Z|, |(mehler r f)''| <= r^2 / b^2 K E|Z^2 - 1|, |d/dr mehler r f x| <= |x| / b K E|Z| + |r| / b^2 K E|Z^2 - 1|; mehler r f and its first two derivatives are continuous. | |||
As t -> +oo, ou t f x tends to the mean of f. As t -> 0 from the right (r -> 1), ou t f x tends to f x for f continuous and bounded, and ou t f tends to f in L^1 of the standard normal law for every bounded measurable f. | |||
Bounded continuous functions are dense in L^1 of the standard normal law: a measurable f with values in [lo, hi] is within eps of a continuous h with values in [lo, hi]. | |||
| brascamp_ | The Gaussian Brascamp-Lieb inequality for bounded functions: for unit vectors u_i of 'rV[R]_m and weights c_i > 0 with sum_i c_i u_i^T u_i = 1, and measurable f_i with values in [delta, K], 0 < delta, \int prod_i f_i(<x, u_i>)^(c_i) dgauss_m <= prod_i (\int f_i dnormal_prob 0 1)^(c_i) (real integrals, powR). Proof by the Ornstein-Uhlenbeck semigroup: \int exp (sum_i c_i ln (mehler r f_i)(<x, u_i>)) dgauss_m is nonincreasing in r on [0, 1], equal to the left side at r = 1 and to the right side at r = 0. | ||
Gaussian integration by parts along a unit vector u: E[<x, u> F(x)] = E[d_u F(x)] for x of law gauss m, F and its derivative d_u F along u bounded and measurable, d_u F continuous along the lines parallel to u. | |||
If sum_i c_i u_i^T u_i = 1 for row vectors u_i of 'rV[R]_m: sum_i c_i <v, u_i> <u_i, w> = <v, w>, so sum_i c_i <v, u_i>^2 = |v|^2; sum_i c_i = m when the u_i are unit vectors; and, for c_i >= 0, |sum_i c_i a_i u_i|^2 <= sum_i c_i a_i^2 for all reals a_i. | |||
Directional derivatives: the chain rule for phi (S x) along a direction v, and the derivative phi' (<x, w>) <v, w> of x |-> phi (<x, w>) along v. | |||
| brascamp_ | The Brascamp-Lieb inequality in Lebesgue form (Ball's geometric form): for unit vectors u_i of 'rV[R]_m and weights c_i > 0 with sum_i c_i u_i^T u_i = 1, and measurable F_i : R -> [0, +oo], \int prod_i F_i(<x, u_i>)^(c_i) dx <= prod_i (\int F_i)^(c_i) (lebesgue_rV m on the left, poweR powers). Proved from gauss_brascamp_lieb applied to F_i(t) sqrt (2 pi) exp (t^2 / 2), with the density gauss_pdf of gauss m. | ||
The Gaussian form for measurable F_i : R -> [0, +oo]: \int prod_i F_i(<x, u_i>)^(c_i) dgauss_m <= prod_i (\int F_i dnormal_prob 0 1)^(c_i), in extended reals with poweR. From gauss_brascamp_lieb_ge0 applied to the truncations min (F_i, k): monotone convergence on the left (the product of the nondecreasing truncated factors converges to the product of the limits, with 0 * +oo = 0), monotonicity on the right. | |||
The Gaussian form for measurable f_i with values in [0, K] (real integrals and powR), from gauss_brascamp_lieb_bounded (values in [delta, K], delta > 0) applied to f_i + 1/(k+1), as k -> oo. |
matrix/48 rows
| 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. |
probability/71 rows
| File | Results | Statement | Used by theories/ |
|---|---|---|---|
| moments.v | Paley-Zygmund: if X is square integrable and 0 <= theta < E X, then P(theta <= X) >= (E X - theta)^2 / E X^2. No sign condition on X. | Head/ | |
Small-ball estimate from the second and fourth moments: if X is in L^4, E X^2 > 0 and 0 <= t < 1, then P(t E X^2 <= X^2) >= (1 - t)^2 (E X^2)^2 / E X^4. | none: Head/ applies paley_zygmund to the square directly | ||
(E X)^2 <= E X^2 for square integrable X. A measurable X with X^2 integrable is in L^2. | Head/; comparison/ in the library | ||
| lindeberg.v | tuple_prod mu n is the law of n independent random elements with laws mu 0, ..., mu (n-1), on n.-tuple T; integrals against it are iterated integrals (Fubini). | none | |
Lindeberg's replacement principle: for F bounded and measurable on n.-tuple T, if replacing the law mu i of coordinate i by nu i changes the expectation of F by at most B i, uniformly in the other coordinates, then replacing all of them changes it by at most B 0 + ... + B (n-1). | none: the proof keeps its own row replacement, Loss/, which works with the iterated expectation on lists; a bridge would need tuple_prod of the standard law to be identified with gaussian_product_law and a reshaping of rows | ||
| subgaussian.v | A random variable X is subgaussian with constant K > 0 when E exp (X^2 / K^2) <= 2, subexponential with constant L > 0 when E exp (|X| / L) <= 2 (Vershynin's psi_2 and psi_1 conditions). A subgaussian X has P(|X| >= u) <= 2 exp (- u^2 / K^2) and E X^(2k) <= 2 k! K^(2k), and every power of X is integrable; a subexponential Y has P(|Y| >= u) <= 2 exp (- u / L). | ||
For E X = 0, E exp (l X) <= exp (3 l^2 K^2) for every l; conversely E exp (l X) <= exp (l^2 s^2) for every l gives the subgaussian condition for every L with 16 s^2 <= 3 L^2. Hoeffding's inequality: for x of law tuple_prod mu n and centered subgaussian f_i (x_i) with constants K_i, sum_i a_i f_i (x_i) is subgaussian with constant 4 (sum_i a_i^2 K_i^2)^(1/2). | |||
X^2 and X Y are subexponential with constants K^2 and K L, Y - E Y with 3 L; for E Y = 0, E exp (l Y) <= exp (16 l^2 L^2) when |l| <= 1 / (2 L). Bernstein's inequality: P(|sum_i a_i f_i (x_i)| >= t) <= 2 exp (- min (t^2 / (64 s^2), t / (4 M))) for independent centered subexponential f_i (x_i), with s^2 = sum_i a_i^2 L_i^2 and M = max_i |a_i| L_i. | |||
| subgaussian_ | A subgaussian constant K of X with E X^2 = 1 is at least 1. Concentration of the norm (Vershynin, Theorem 3.1.1): for x of law tuple_prod mu n and f_i (x_i) subgaussian with constant K and E f_i (x_i)^2 = 1 (not necessarily centered), P(|(sum_i f_i (x_i)^2)^(1/2) - sqrt n| >= t) <= 2 exp (- t^2 / (576 K^4)) for t >= 0. | ||
P(|X| >= r) <= 2 exp (- r^2 / (4 s^2)) when E exp (l X) <= exp (s^2 l^2) for every l. For a random m x n matrix A with measurable entries (then opnorm A is measurable) whose bilinear forms u^T A v, |u|, |v| <= 1, satisfy that bound, P(opnorm A > 12 s (sqrt m + sqrt n + t)) <= 2 exp (- t^2) for t >= 0, by nets of the unit balls. For independent centered entries subgaussian with constant K (Vershynin, Theorem 4.4.5): P(opnorm A > 21 K (sqrt m + sqrt n + t)) <= 2 exp (- t^2). | |||
| mixture.v | The finite mixture of probabilities P i (i in a finite type) with weights w i >= 0 of sum one, a probability; for f nonnegative and measurable, or integrable under every P i, int f d(mixture) = sum_i w_i int f dP_i, and an integrable (square integrable) variable under every P i is so under the mixture. | ||
The law of total variance, Var X = sum_i w_i (Var_i X + (E_i X - E X)^2), for X square integrable under every P i (X \in Lfun (P i) 2); a variable subgaussian (subexponential) with constant K under every P i is so under the mixture; the image of a mixture by a measurable map is the mixture of the images; measurable sets E i with P i (E i) <= eps that all contain F have a measurable intersection, containing F, of mixture probability at most eps. | |||
sum_(s : n-tuples) prod_k F k (s_k) = prod_k sum_i F k i, so the product weights prod_k w (s_k) of the label tuples are mixture weights; the product tuple_prod of n copies of a mixture is the mixture, over the label tuples s, of the products tuple_prod (fun k => P (s_k)) n. | |||
| countable_ | The countable mixture of probabilities P s, s : nat, with weights p s >= 0 of sum one (\sum_(s <oo) p s = 1), a probability: the measure series of the scaled P s. For f nonnegative and measurable, and for f integrable under every P s with sum_s p_s int |f| dP_s < +oo, int f d(mixture) = sum_s p_s int f dP_s; in the second case f is integrable under the mixture. | ||
The weight r_m = sum_(s > m) p_s of the labels above m, with sum_(s <= m) p_s + r_m = 1; r_m is at most any eps > 0 for some m. For r_m > 0 the weights p_s / r_m, s > m, are mixture weights (the normalized tail sum_(s > m) p_s P_s / r_m), and a series of nonnegative terms against them is 1 / r_m times the series over s > m against p. | |||
For nonnegative terms, esum (c x_i) = c esum x_i (c >= 0); an esum over a subset of a finite type is a finite sum; if the esum over nat of the nonnegative a_i is a real number x_i for every i < n, the esum over s : n.-tuple nat of prod_i a_i (s_i) is prod_i x_i (the countable form of big_tuple_distr), in particular x^n when every a_i is a. Hence the product weights prod_i p (s_i) of the label tuples have sum one, and sum (1 - r_m)^n over the tuples whose labels are all at most m (labels_le n m). | |||
The coupling of label tuples. A mixture esum_(s : n.-tuple nat) prod_i p (s_i) Q_s(A) and a finite mixture sum_(t : n.-tuple 'I_N) prod_i q (t_i) Q'_t(A), m < N, whose weights and probabilities agree on the tuples with all labels at most m, differ by at most 1 - (1 - r_m)^n on every measurable A; and 1 - (1 - r)^n <= n r for 0 <= r <= 1. | |||
n independent draws from a countable mixture: for weights p with cmixture_weights p, probabilities P s (s : nat) and every measurable set A of n-tuples, tuple_prod (fun=> cmixture P hp) n A is the esum over the label tuples s : n.-tuple nat of prod_k p (s_k) times tuple_prod (fun k => P (s_k)) n A; the countable form of tuple_prod_mixture. | |||
| total_ | The total variation distance of two probabilities P and Q on a measurable type: tv_dist P Q = sup {|P A - Q A| : A measurable}, a real number. For every measurable A, |P A - Q A| <= tv_dist P Q, as reals and as extended reals, and tv_dist P Q is the least such bound; as an extended real it is the ereal_sup of the |P A - Q A|. | ||
A pseudometric with values in [0, 1]: symmetric, with the triangle inequality, and zero for laws that agree on the measurable sets. | |||
For laws mu i and nu i on T and every measurable set A of n-tuples, |tuple_prod mu n A - tuple_prod nu n A| <= sum_(i < n) tv_dist (mu i) (nu i): the hybrid argument of lindeberg_replacement, with the indicator of A. | |||
For 0 <= x < n, exp (- x n / (n - x)) <= (1 - x / n)^n <= exp (- x) and |(1 - x / n)^n - exp (- x)| <= x^2 / (n - x); hence (1 - x / n)^n tends to exp (- x) for every x >= 0. | |||
| atoms.v | On a measurable type whose singletons are measurable, the atoms of a measure P are the points x with P [set x] != 0. A finite measure has countably many atoms, and a countable set without atoms is null. Hence, for sets S x such that every S x and every [set x | S x y] is countable, the points x with P (S x) != 0 form a countable set, for a finite measure P. | ||
For a measure P, a probability Q and a set A of pairs whose vertical and horizontal sections are countable, there is a countable set N of first coordinates with (P \x Q) (A minus N x T2) = 0. If moreover P is a probability without atoms and A is measurable, then (P \x Q) A = 0. | |||
| efron_ | Fubini at one coordinate of tuple_prod mu n: resampling coordinate i by an independent t of law mu i (tuple_set x i t) does not change the integral; coordinate i has law mu i, and E[f (x_i) H (x)] = E[f] E[H] when H does not depend on x_i. | ||
The Efron-Stein inequality: Var F <= sum_i E Var_(x_i) F = 1/2 sum_i E (F (x) - F (x^(i)))^2 for F square integrable under tuple_prod mu n, x^(i) being x with coordinate i resampled; E (X - X')^2 = 2 Var X for an independent copy; (int |f g|)^2 <= int f^2 int g^2. | |||
The L^4 step of the moment recursion of Koehler and Sohn (proof of their Proposition 2.6): if E (F (x) - F (x^(i)))^4 <= D_i^2 for every i, then E (F - E F)^4 <= 9/2 (sum_i D_i)^2. | |||
| efron_ | The omission form of the Efron-Stein inequality (Steele): for x of law tuple_prod mu n, F integrable (or measurable and bounded) and G i measurable with G i (tuple_set x i t) = G i x for all x and t (G i does not depend on the coordinate i), Var F <= sum_i E (G i - F)^2, in [0, +oo]. The lemma 'Deletion variance bound' of family 235 of the OpenAI math collection, in general form. | ||
| finite_ | Means and variances under the uniform law of a finite type, as finite averages over a realFieldType: linearity, monotonicity, invariance under bijections, the mean of the indicator of a predicate as the proportion of the elements that satisfy it, Fubini for pairs, the mean over m.+1.-tuple T as the mean over the head of the mean over the tail, the mean of a product over independent coordinates as the product of the means, the law of T1 + T2 as a mixture with weights #|T1| and #|T2| (the cardinals of T1 and T2), Var f <= E (f - c)^2, Jensen (E f)^2 <= E f^2 and the law of total variance for a pair and for the head of a tuple (nonempty types where needed). | ||
| tuple_ | Fubini for tuple_prod mu n: for the first coordinate (nonnegative or integrable functions), for a first and a last block of coordinates, which are therefore independent with the product laws of their coordinates; the integral of prod_i f_i (x_i) is the product of the integrals. | ||
A tuple of n * m coordinates read as n rows of m: under tuple_prod mu (n * m) the rows are independent, row i with law tuple_prod (fun j => mu (i * m + j)) m. Coordinatewise maps preserve independence: if mu i is the image of nu i under g i, tuple_prod mu n is the image of tuple_prod nu n under tuple_map g. | |||
| variational.v | For a law mu on the line with a finite second moment, the upper partial moments m(w) = E (X - w)_+ and s(w) = E (X - w)_+^2: m is nonincreasing and 1-Lipschitz, E X - w <= m(w) <= E X^2 / (4 w) for w > 0, m(w) > 0 if mu(]b, +oo[) > 0 for some b > w, and |s(w + h) - s(w) + 2 h m(w)| <= h^2, so s' = -2 m. | ||
For c > -1, the equation w + z = c m(w) has exactly one solution, upper_cutoff mu c z = sup {w | w + z <= c m(w)}, and the half-line {w | w + z <= c m(w)} is ]-oo, upper_cutoff mu c z] (Koehler-Sohn, Lemma 5.7). | |||
For c > -1, the energy E = s + c m^2 satisfies E(w1) - E(w2) >= 2 min(1, 1 + c) m(w2) (w2 - w1) for w1 <= w2: it is strictly decreasing where m > 0; |E(a) - E(b)| <= 2 (1 + |c|) m(a) (b - a) for a <= b, so E is continuous; and E(w) >= (1 + c) m(w)^2 for every c. | |||
For a law with a finite second moment, clip_energy mu C t = s(-t) + s(C t), which for a symmetric law is the mean of (t - X)_+^2 + (X - C t)_+^2, the mean squared distance from X to [t, C t] when t <= C t (for example C >= 1 and t >= 0), and its infimum clip_value mu C over t >= 0. Its derivative in t is 2 (m(-t) - C m(C t)) (a Taylor bound with remainder (1 + C^2) h^2), so a t0 >= 0 where the derivative is <= 0 before and >= 0 after is a minimum. It is nonincreasing in C, with 0 <= clip_energy C t - clip_energy C' t <= (C' - C) t (m(C t) + m(C' t)) for C <= C'. The tool: a function with |F(t + h) - F(t) - h g(t)| <= K h^2 for h >= 0 is nonincreasing where g <= 0 and nondecreasing where g >= 0. | |||
Lemma 5.7 of Koehler and Sohn: for c > -1 and w the cutoff, the supremum of (E (X + z) f(X))_+^2 / (E f(X)^2 + c (E f(X))^2) over measurable f >= 0 with E f^2 < oo and E f > 0 is s(w) + c m(w)^2, attained at f(x) = (x - w)_+ when positive. | |||
The value z |-> s(w_z) + c m(w_z)^2 is nondecreasing, and strictly increasing where it is positive. | |||
Lemma 5.8 of Koehler and Sohn, quantitatively: the cutoff and the value of a law mu differ from those of nu by explicit amounts that depend only on m_mu, s_mu, m_nu, s_nu at the cutoff of nu; so if m_{mu_n} and s_{mu_n} converge to m_mu and s_mu at the cutoff of mu (no local uniform convergence needed), the cutoffs and the values converge. | |||
For a law invariant under x |-> -x with E X^2 = v: m(-w) = m(w) + w, s(-w) + s(w) = v + w^2, and for c > -1, c' = -c / (1 + c), z' = -z / (1 + c), the cutoff of (c', z') is minus that of (c, z) and the two values add up to v + z^2 / (1 + c) (the scalar part of Lemma 5.9); at z = 0 the variational bound holds without the positive part, (E X f(X))^2 <= value (E f(X)^2 + c (E f(X))^2) (Proposition 5.10 (ii)). | |||
(E g)^2 <= E g^2; a quadratic polynomial a + 2 b t + k t^2 that is nonnegative for all t, with k >= 0, has b^2 <= a k; a law invariant under x |-> -x makes f(-X) integrable with f(X) and gives E f(-X) = E f(X). | |||
The empirical law of a nonempty list s of reals, the average of the Dirac masses at its elements, is a probability on the line; integrals against it are averages over s, so the upper partial moments of the empirical law of g_1, ..., g_d are (1/d) sum_i (g_i - w)_+^k. | |||
The finite form of Lemma 5.7 of Koehler and Sohn for c >= 0, with weights that need not be functions of the values: for r_i >= 0, (1/d) sum_i (g_i + z) r_i <= sqrt V ((1/d) sum_i r_i^2 + c ((1/d) sum_i r_i)^2)^(1/2), V the value of the empirical law of the g_i, with equality at r_i = (g_i - w)_+, w the cutoff. | |||
| clip_ | For a law mu on the line, symmetric with a finite second moment, reals C >= 1, t >= 0 and a, the clipped profile q(x) = min (max (x - a) t) (C t) is admissible (measurable, with t' <= q <= C t' for some t' >= 0), equals t + (x - t - a)_+ - (x - C t - a)_+, is the point of [t, C t] closest to x - a, and has mean t + m(t + a) - m(C t + a); clip_objective mu c q = 2 E[X q(X)] - E[q(X)^2] - c (E q(X))^2. | ||
Under the balance m(-(t + a)) = C m(C t + a), the residual w(x) = x - a - q(x) satisfies E[w (q' - q)] <= 0 for every admissible q' and E[w q] = 0; if moreover a = c E q(X) with c > -1, then q maximizes clip_objective mu c over the admissible profiles, and its value is E[X q(X)] = J(t + a) - J(C t + a), J(w) = s(w) + w m(w). | |||
The shifted clipping energy s(-t - a) + s(C t + a) is the mean squared distance from X - a to [t, C t], and under the balance it is minimal over t' >= 0 at t. The dual D(b) = E X^2 + c (1 + c) b^2 - inf_(t' >= 0) (s(-t' - c b) + s(C t' + c b)) satisfies, under the balance and the fixed point: D(E q(X)) = clip_objective mu c q, D(b) <= clip_objective mu c q for every b if -1 < c <= 0, clip_objective mu c q <= D(b) for every b if c >= 0 (this direction for every clipped profile), and 0 <= E q(X) with min(1, 1 + c)^2 (E q(X))^2 <= E X^2. | |||
For bounded measurable q and h, clip_objective mu c (q + h) = clip_objective mu c q + 2 E[(X - c E q(X) - q(X)) h(X)] - E[h(X)^2] - c (E h(X))^2; under the balance and the fixed point, the clipped profile q has clip_objective mu c q = E[q(X)^2] + c (E q(X))^2; a profile admissible for C is admissible for every C' >= C. | |||
For every law mu on the line and all reals c and C: two measurable profiles equal mu-almost everywhere have the same clip_objective mu c. If q is measurable and t <= q <= C t holds mu-almost everywhere for some t >= 0 (clip_admissible_ae mu C q), then the clipped profile min(max(q, t), C t) is admissible for C, equals q almost everywhere and has the objective of q. So clip_objective mu c takes the same values on the admissible profiles and on those admissible almost everywhere, and has the same supremum on the two classes. If mu has a finite second moment, then q, x q(x) and q(x)^2 are integrable for every q admissible almost everywhere. | |||
| semicircle_ | The semicircle law of radius r, of density 2 / (pi r^2) sqrt (r^2 - x^2) on [-r, r], is a probability (for r = 0 the density is the indicator of [0, 1], as for normal_pdf m 0); the half disk has area pi a^2 / 2, computed by the substitution x = a sin t. | ||
Integrating against the semicircle law is integrating against Lebesgue measure with its density, over [-|r|, |r|], also for a function g that agrees with f where the density is positive; every continuous function f is integrable, and so is f times the density. | |||
For r != 0 the law is invariant under x |-> -x, every half-line ]b, +oo[ with b < |r| has positive probability, and a function f with f times the density integrable has a measurable restriction to ]-|r|, |r|[ with the same products with the density. | |||
Moments: E X^(k+2) = (k + 1) r^2 / (k + 4) E X^k (integration by parts), so the odd moments vanish, E X^2 = r^2 / 4, and at r = 2 the even moments are the Catalan numbers. | |||
The semicircle laws form a scale family: a p_{a r}(a x) = p_r(x), and int f(a x) dsigma_r(x) = int f dsigma_{a r} for a > 0 and f >= 0 measurable. | |||
| symmetrization.v | Rademacher averages are averages over the 2^n sign vectors. Ledoux-Talagrand contraction: for L-Lipschitz phi_k with phi_k(0) = 0 and a finite class of vectors t_j, E max_j |sum_k eps_k phi_k(t_jk)| <= 2 L E max_j |sum_k eps_k t_jk|; and E |sum_k a_k eps_k| <= (sum_k a_k^2)^(1/2). | ||
Gine-Zinn symmetrization: for x of law tuple_prod mu n and a finite class of measurable f_j integrable for every mu k, E max_j |sum_k (f_j(x_k) - E f_j(x_k))| <= 2 E rademacher_mean (max_j |sum_k eps_k f_j(x_k)|), as integrals in [0, +oo]. | |||
| small_ | Mendelson's small-ball method in Markov form, for x of law tuple_prod mu n: if the measurable f_j satisfy mu_k(|f_j| >= 2 u) >= q and E rademacher_mean (max_(j < J) |(1/n) sum_k eps_k f_j(x_k)|) <= r for every J, the probability that some f_j has sum_k f_j(x_k)^2 < n u^2 q / 2 is at most 8 r / (u q). By symmetrization, contraction and Markov's inequality, without a concentration inequality. | ||
For linear forms <F(t), p> with p in a set D, E <F, p>^2 = p S p^T > 0, E <F, p>^4 <= K (p S p^T)^2, and a measurable Psi with |(1/n) sum_k eps_k <F(x_k), p>| <= sqrt (p S p^T) Psi(x, eps) and E rademacher_mean Psi <= r: outside a measurable event of probability at most 512 K r / 9, (1/n) sum_k <F(x_k), p>^2 >= 9 / (512 K) p S p^T for every p in D. Also: P(|X| >= 1/2) >= 9 / (16 K) if E X^2 = 1 and E X^4 <= K; every nonempty set of row vectors contains a dense sequence. | |||
| conditioning.v | Conditioning tuple_prod mu n on the coordinates in a set S by resampling the others: tuple_merge S x y takes the coordinates in S from x and the others from y, and its law under two independent copies of tuple_prod mu n is tuple_prod mu n. If H depends only on the coordinates in S (H (tuple_merge S x y) = H x) and, for every x in H, tuple_merge S x y is in E with probability at most c x, then P(E and H) <= int_H c. | ||
Events that depend on pairwise disjoint sets of coordinates are independent. Revealing the coordinates in nested sets S 0, S 1, ...: if A l depends only on the coordinates in S (l + 1) and, given those in S l of a tuple of A 0, ..., A (l - 1), has probability at most c l, then P(A 0, ..., A (L - 1)) <= c 0 ... c (L - 1). | |||
For an injective f : 'I_k -> 'I_n, the coordinates f 0, ..., f (k - 1) of tuple_prod mu n have the law tuple_prod nu k with nu i = mu (f i). The measure of a box is the product of the measures of its sides, and two finite measures on n.-tuple T that agree on the boxes agree. | |||
| density_ | For a probability mu and a measurable f >= 0 with int f dmu = 1 (prob_density mu f), density_prob mu f is the probability A |-> int_A f dmu, absolutely continuous with respect to mu; it is mu itself when f is not such a density. | ||
Integrating g against density_prob mu f is integrating g f against mu, for g nonnegative or integrable. A density may be changed on a mu-null set, even to negative values: int_A f' dmu = density_prob mu f A when f' = f mu-almost everywhere. | |||
If f_k is a density against nu_k for every k < n, the product of the laws density_prob nu_k f_k has the density x |-> prod_k f_k (x_k) against tuple_prod nu n. | |||
The constructor with a proof that f is a density: for hf : prob_density mu f, density_law mu f hf is the probability A |-> int_A f dmu, by definition and with no fallback to mu. It is density_prob mu f, and integrals against the two agree; density_law_dominates, ge0_integral_density_law, integrable_density_law, integral_density_law, eq_density_law and tuple_prod_density_law restate the three rows above for it. | |||
| hanson_ | The Hanson-Wright inequality: for x of law tuple_prod mu n with X_i = f_i (x_i) centered and subgaussian with constant K, and A a real n x n matrix, Q = \sum_(i, j) a_ij X_i X_j satisfies P(|Q - E Q| >= u) <= 2 exp (- min (u^2 / (6912 K^4 |A|_F^2), u / (136 K^2 opnorm A))), and Q - E Q is subexponential with constant 252 K^2 |A|_F; E Q is written \sum_i a_ii E X_i^2 (hw_center). Proved by decoupling over the sets S of coordinates, Hoeffding's inequality twice and a Gaussian chaos bound, and Bernstein's inequality for the diagonal. | ||
For g of law gauss n: E exp <g, w> = exp (|w|^2 / 2), and E exp (t |g M|^2) <= exp (3/2 t |M|_F^2) when 4 t opnorm M ^ 2 <= 1. A bound E exp (l Y) <= exp (l^2 s^2) for |l| b <= 1 makes Y subexponential with constant 3 max (2 s, b). The off-diagonal sum \sum_(i != j) c_ij is 4 / 2^n times the sum over the sets S of \sum_(i in S, j notin S) c_ij. | |||
| measurable_ | Measurable selection of minimizers: if g t has a minimizer th t on D with quadratic growth g t (th t) + c |theta - th t|^2 <= g t theta for theta in D (c > 0), and the values g t (q m) at a fixed sequence q of points of D are measurable in t and come arbitrarily close to the minimum, then t |-> th t is measurable (the limit of the first minimizers among q 0, ..., q k). A nonempty relatively open convex set has a dense sequence of points. Hence the minimizer over D x R of the least squares objective with a self-concordant barrier of convex/ is a measurable function of the features; the reduced objective grows by at least beta lambda |theta - ls_min Z|^2 away from it, and it does not depend on the features that the objective does not use, as for a leave-one-out objective. | ||
| log_ | For a nonempty finite type X, weights w x > 0 and functions h x of a real parameter t: the derivative of the log-partition function ln (sum_x w x exp (h x t)) is the Gibbs mean of h', and the derivative of the Gibbs mean of q is the mean of h' q + q' minus the product of the means of q and h'. So if the h x have three derivatives with |h'| <= b1, |h''| <= b2 and |h'''| <= b3, the log-partition function has three derivatives and the third is at most b3 + 6 b1 b2 + 6 b1^3 in absolute value. A Gibbs mean of q is at most the bound of q in absolute value (gibbs_mean_le). | ||
| rademacher_ | Lindeberg's replacement of uniform signs by Gaussians (Chatterjee 2006, Theorem 1.1, for signs and standard Gaussians): if F : 'rV[R]_n -> R is measurable and bounded, and for every x and j the map t |-> F (t e_j + x) has three derivatives with the third at most c_j in absolute value, then the average of F over the 2^n rows of signs and its integral against gauss n differ by at most (1/2) sum_j c_j. By induction on n, with Fubini along rV_cons for bounded measurable functions (Rintegral_gauss_cons) and the decomposition of the rows of signs by their first coordinate (sum_sign_rowS). | ||
The mean value inequality |g b - g a| <= k b - k a for a <= b and g, k differentiable everywhere with |g'| <= k' on [a, b], and Taylor's formula of order two: |f t - f 0 - f'(0) t - f''(0) t^2 / 2| <= c |t|^3 / 6 when |f'''| <= c everywhere. In one coordinate, |(f 1 + f (-1)) / 2 - E f(g)| <= c / 2 for g of law N(0, 1), from E (a + b g + c g^2) = a + c and E |g|^3 <= 2. | |||
| finite_ | Spectral gaps on a finite space. For a finite type X, weights w x > 0 and an operator L on the functions on X that is linear, self-adjoint in L^2(w) (<f, L g>_w = <L f, g>_w, with <f, g>_w = sum_x w x f x g x) and nonnegative (<f, L f>_w >= 0): if k <f, L f>_w <= <L f, L f>_w for every f, then k <f, f>_w <= <f, L f>_w for every f orthogonal to the kernel of L. If moreover the weights sum to one and the kernel of L is the constants, then k Var_w(f) <= <f, L f>_w for every f (a Poincare inequality). A Rocq formalization of the credited argument of a proposition of family 227 of the OpenAI math collection (see the header). | ||
The isometry f |-> (sqrt (w x) f x)_x of L^2(w) onto 'cV[R]_#|X| and its inverse, and the matrix wop_mx w L of an operator in the corresponding basis: wop_mx w L *m wvec f = wvec (L f) and u^T (wop_mx w L) u = <wfun u, L (wfun u)>_w for a linear L, symmetric when L is self-adjoint. |
fourier/50 rows
| File | Results | Statement |
|---|---|---|
| charfun.v | The characteristic function of a law mu on R (a probability on measurableTypeR R, the type of normal_prob), without complex numbers: cf_re mu t = E[cos (t X)], cf_im mu t = E[sin (t X)] for X of law mu, the pair cf mu t of the two, and its modulus cf_norm mu t. A pair (a, b) stands for a + i b: cmul is the complex product and cmod the modulus, which is multiplicative (cmodM, cmod_prod). | |
cf mu 0 = (1, 0), cf mu (- t) is the conjugate of cf mu t, the modulus is at most one, and the three functions are continuous in t. | ||
If nu is the law of a measurable g : T -> R under a probability P (P (g @^-1` A) = nu A for measurable A), then cf nu t = (E_P[cos (t g)], E_P[sin (t g)]). | ||
The law of a X + b has the characteristic function exp (i b t) cf mu (a t), of modulus cf_norm mu (a t). | ||
Independent sums: for independent X1, X2 (laws P1, P2, joint law P1 \x P2) and measurable g1, g2, the characteristic function of g1 X1 + g2 X2 is the complex product of those of g1 X1 and g2 X2, so the moduli multiply. | ||
For x of law tuple_prod mu n (independent coordinates of laws mu 0, ..., mu (n-1)) and reals a k, the characteristic function of \sum_k a_k x_k at t is the complex product of the cf (mu k) (a_k t), and its modulus is the product of the cf_norm (mu k) (a_k t). | ||
Symmetrization: the law of X - X', for independent X and X' of law mu, has the real characteristic function cf_norm mu t ^ 2. | ||
For s != 0, the characteristic function of normal_prob m s at t is expR (- (s t)^2 / 2) (cos (m t), sin (m t)), of modulus expR (- (s t)^2 / 2). Proved for the standard law by differentiating under the integral and Stein's identity (normal_ibp), which give y' = - t y, then by cf_affine. | ||
| Fubini for a bounded measurable real function on a product of two probabilities. | ||
Derivatives of s |-> cos (t s), sin (t s), cos (s z) and sin (s z). | ||
| esseen.v | The Levy concentration function Q(mu, L) = sup_a mu [a, a + L] of a law on the line: between 0 and 1, nondecreasing in L, and Q(mu, L) <= (L / L' + 1) Q(mu, L') for 0 <= L and 0 < L'. | |
Adding an independent variable does not increase the concentration function: if nu is the law of g X + e Y for X of law P independent of Y of law mu and e != 0, then Q(nu, |e| L) <= Q(mu, L). | ||
Jordan's inequality 2 x / pi <= sin x on [0, pi / 2], hence 1 - cos u >= 2 u^2 / pi^2 for |u| <= pi. | ||
The integral of the triangle kernel: \int_0^T (1 - t / T) cos (t z) dt = (1 - cos (T z)) / (T z^2) (T / 2 at z = 0); it is nonnegative, and at least 2 T / pi^2 for |z| <= pi / T. | ||
Esseen's inequality: for every law mu on the line and T > 0, Q(mu, 2 pi / T) <= pi^2 / (4 T) \int_{-T}^T |cf mu t| dt = pi^2 / (2 T) \int_0^T |cf mu t| dt. | ||
Concentration of sums: for independent X_1, ..., X_n (n >= 1, laws mu_k, tuple_prod) with E[X_k^2] <= v and Q(mu_k, lambda) <= 1 - eps, the law of X_1 + ... + X_n satisfies Q(S, L) <= 2 pi^2 sqrt pi (L + sqrt (v / eps)) / (lambda sqrt (eps n)) for L >= 0. | ||
Symmetrization, for X, X' independent of law mu (on mu \x mu): P(|X - X'| < lambda / 2) <= Q(mu, lambda), E[(X - X')^2] <= 4 E[(X - a)^2] for every a, Markov's tail bound, |cf mu t|^2 = E[cos (t (X - X'))], and, if Q(mu, lambda) <= 1 - eps, E[X^2] <= v and 8 v <= eps r^2, then |cf mu t|^2 <= 1 - lambda^2 eps t^2 / (4 pi^2) for |t| <= pi / r. | ||
| Fubini for real integrals against a probability and a sigma-finite measure, for a measurable function dominated by an integrable function of the second variable; both partial integrals are measurable. | ||
The fundamental theorem of calculus for an antiderivative on the whole line; \int_{-T}^T f = 2 \int_0^T f for f even and continuous; \int_0^T exp (- (c t)^2) dt <= sqrt pi / (2 c). | ||
| gauss_ | Lemma 3.5 of Koehler and Sohn: for a law mu on the line with E[X^2] <= v and Q(mu, lambda) <= 1 - eps (v, lambda, eps > 0), and for 0 < r <= 1/2 and r <= s, \int |cf mu u|^(1/r^2) exp (- s^2 u^2 / (2 r^2)) du <= r C (an integral in [0, +oo]), with C = 16 pi^3 sqrt pi e^(1/8) (1 + sqrt (4 v / eps)) / (lambda sqrt eps). | |
The same bound after the substitution u = r t: \int |cf mu (r t)|^(1/r^2) exp (- s^2 t^2 / 2) dt <= C; the form with a constant C > 0 uniform in mu, r and s for 0 < r <= s <= 1/2; and both with the centered moment E[(X - a)^2] <= v for any a (the variance when a is the mean) in place of E[X^2] <= v, with the same constant. | ||
The first half of the same lemma, for any truncation level c: a law with mean 0, variance 1 and E[X^2 1_{|X| <= M}] >= c (M > 0) satisfies Q(mu, L) <= 1 - min ((c - 4 L^2) / M^2, L^2 / (2 L^2 + 1)) for every L > 0, a bound with a positive constant when 4 L^2 < c. For c = 1/2 and L = 1/8, the paper's form: Q(mu, 1/8) <= 1 - min (7 / (16 M^2), 1/100). | ||
The Gaussian Fubini identity \int cf_re nu u exp (- u^2 / 2) du = sqrt (2 pi) E[exp (- X^2 / 2)] for X of law nu; the bound E[exp (- X^2 / 2)] <= 2 e^(1/8) sqrt (2 pi) Q(nu, 1); \int exp (- y^2 / 2) dy = sqrt (2 pi); E[f (G)] = \int f phi for G standard normal and f bounded measurable. | ||
The law of X - X' for X, X' independent of law mu, and the law of a sum of independent variables (tuple_prod): cf (sym_law mu) t = (|cf mu t|^2, 0), Q(sym_law mu, L) <= Q(mu, L), E[(X - X')^2] <= 4 E[X^2], and the sum of n independent copies of X - X' has real characteristic function |cf mu t|^(2 n). | ||
| charfun_ | The characteristic function of a law nu on 'rV[R]_m at theta, without complex numbers: cf_rV_re nu theta = E[cos <x, theta>] and cf_rV_im nu theta = E[sin <x, theta>] for x of law nu, with <x, theta> = mxdot x theta; it is the characteristic function at 1 of the law of <x, theta>. | |
The modulus is at most one, and the three functions are continuous, hence measurable, in theta. | ||
The characteristic function of gauss m at theta is (exp (- mxdot theta theta / 2), 0). | ||
If nu is the law of g under P, cf_rV nu is computed under P. The law of the sum of independent vectors (under nu1 \x nu2) has the complex product of their characteristic functions. For x of law tuple_prod mu n and vectors w k, the law of \sum_k x_k w_k has at theta the complex product of the cf (mu k) <w k, theta>, so its modulus is the product of the cf_norm (mu k) <w k, theta>. | ||
| Fubini for a bounded measurable function on a product of two probabilities: the two iterated integrals agree. | ||
The law of y + s G, for G of law gauss m and s > 0, has the density w |-> s^-m gauss_pdf ((w - y) / s) with respect to lebesgue_rV m. | ||
Gaussian regularization: for Y of law nu, G of law gauss m and s > 0, E[exp (- |z - Y|^2 / (2 s^2))] = E[cos <G/s, z> cf_rV_re nu (G/s) + sin <G/s, z> cf_rV_im nu (G/s)], hence it is at most (s / sqrt (2 pi))^m \int |cf_rV nu theta| exp (- s^2 |theta|^2 / 2) dtheta, where |.| is the Euclidean norm. | ||
For Y of law nu and an independent G of law gauss m, s > 0 and a measurable B, P(Y + s G in B) <= (2 pi)^-m (\int |cf_rV nu theta| exp (- s^2 |theta|^2 / 2) dtheta) lebesgue_rV m B, with values in [0, +oo]. No Fourier inversion is used. | ||
If \int |cf_rV nu| < +oo, every closed Euclidean ball B of radius r > 0 satisfies nu B <= (2 pi)^-m (\int |cf_rV nu theta| dtheta) lebesgue_rV m B: prod_gauss_le_cf_rV with s -> 0. | ||
Closed Euclidean balls are measurable, and scaling the radius by a > 0 multiplies their Lebesgue measure by a^m. For G of law gauss m, E[|G|^2] = m and P(|G| <= t) >= 1 - m / t^2. | ||
| small_ | Products of nonnegative extended reals are monotone, and x^(\sum_i c_i) = \prod_i x^(c_i) for x > 0. | |
For a frame of 'rV[R]_m (\sum_k w_k^T w_k = I_m): |theta|^2 = \sum_k <theta, w_k>^2 and \sum_k |w_k|^2 = m. | ||
For x of law tuple_prod mu n and a frame w, the regularized modulus exp (- s^2 |theta|^2 / 2) |cf_rV nu theta| of the law nu of \sum_k x_k w_k is the product over k of |cf mu_k <w_k, theta>| exp (- s^2 <w_k, theta>^2 / 2). | ||
Removing the Gaussian: for G of law gauss m independent of Y (law nu) and 2 m s^2 <= d^2, P(|Y - z| <= r) <= 2 P(|Y + s G - z| <= r + d). With prod_gauss_le_cf_rV and the volume of the ball: if \int exp (- s^2 |theta|^2 / 2) |cf_rV nu theta| dtheta <= C^m, C >= 0 and 2 s^2 <= eta^2, then P(|Y - z| <= eta sqrt m) <= (sqrt (8 e / pi) C eta)^m. | ||
Whitening: if |x W| <= |x| for all x, then |y W^T| <= |y|; the event |\sum_k x_k w_k - z| <= t is then contained in the same event for the vectors w_k W^T and the center z W^T, and if W (\sum_k w_k^T w_k) W^T = I_m the w_k W^T form a frame. | ||
The Brascamp-Lieb inequality in Lebesgue form with nonnegative weights, unit vectors being required only where the weight is positive, from the form with positive weights (brascamp_lieb of comparison/) by reindexing. | ||
Lemma 3.8 of Koehler and Sohn: for a frame w and the law nu of \sum_k x_k w_k, x of law tuple_prod mu n, if \int |cf mu_k u|^(1 / r^2) exp (- s^2 u^2 / (2 r^2)) du <= r C at r = |w_k| for each nonzero w_k, then \int exp (- s^2 |theta|^2 / 2) |cf_rV nu theta| dtheta <= C^m. By Brascamp-Lieb with u_k = w_k / |w_k|, c_k = |w_k|^2, and the change of variables u = |w_k| t. | ||
The vector small-ball estimate with an explicit constant: if W (\sum_k w_k^T w_k) W^T = I_m, |x W| <= |x|, |w_k| <= rho and the laws mu_k satisfy the bound of the previous row with constant C for all 0 < r <= s <= 1/2 (Lemma 3.5 of the paper), then P(|\sum_k x_k w_k - z| <= eta sqrt m) <= (K eta)^m for eta >= K rho, with K = max (2, sqrt (8 e / pi) C). | ||
The vector small-ball estimate: for v, lambda, eps > 0 there is C > 0 such that for independent x_1, ..., x_n (laws mu_k, tuple_prod) with E[x_k^2] <= v and conc_fun mu_k lambda <= 1 - eps, row vectors w_k of 'rV[R]_m with \sum_k <x, w_k>^2 >= |x|^2 for all x and |w_k| <= rho, every eta >= C rho and every z, P(|\sum_k x_k w_k - z| <= eta sqrt m) <= (C eta)^m. | ||
The same in the form of Proposition 2.4 of Koehler and Sohn: for laws of mean zero and variance one with E[x^2 1_{|x| <= M}] >= 1/2, the constant depends only on M. | ||
The same for laws of mean zero and variance one with E[x^2 1_{|x| <= M}] >= c, for any level c > 0; the constant depends only on M and c. | ||
The vector small-ball estimate with E[(x_k - a_k)^2] <= v in place of E[x_k^2] <= v, for any centers a_k (the means, for the variance form); same constant as vector_small_ball. | ||
| inversion.v | The Fourier inversion theorem on row vectors: if \int |cf_rV nu theta| dtheta < +oo against lebesgue_rV m, then nu X = \int_X cf_rV_density nu w dw for every measurable X, with cf_rV_density nu w = (2 pi)^-m \int (cos <theta, w> cf_rV_re nu theta + sin <theta, w> cf_rV_im nu theta) dtheta. | |
The density is bounded by (2 pi)^-m \int |cf_rV nu|, continuous, nonnegative and of integral one; cf_rV_inv_prob h is the probability it defines. | ||
Gaussian regularization of the density: for s > 0, (2 pi)^-m \int exp (- s^2 |theta|^2 / 2) (...) dtheta is the density s^-m E[gauss_pdf ((w - Y) / s)] of Y + s G, it is the average of cf_rV_density nu over w + s G, and it tends to cf_rV_density nu w as s -> 0. | ||
For any law mu on 'rV[R]_m and G of law gauss m: E[phi (Y + s G)] = s^-m \int phi w E[gauss_pdf ((w - Y) / s)] dw for nonnegative measurable phi, and |E[phi (Y + s G)] - E[phi Y]| <= |L| s (1 + m) / 2 for phi with values in [0, 1] and Lipschitz with constant L. |
convex/35 rows
| File | Results | Statement |
|---|---|---|
| self_ | Self-concordant functions and barriers (Nesterov-Nemirovskii; Koehler-Sohn, Definition 2.7) on a convex set D of 'rV[R]_N that is relatively open in z + V for a subspace V: derivatives along the directions of V (MathComp's 'D_h) up to order 3, a gradient vector and a Hessian matrix, convexity, (D^3 B[h,h,h])^2 <= 4 (D^2 B[h,h])^3, and B tends to +oo along segments that leave D; a theta-barrier also has (D B[h])^2 <= theta D^2 B[h,h]. sc_norm B z h is the local norm sqrt (D^2 B(z)[h,h]), bregman_div B y z = B y - B z - D B(z)[y - z]. | |
Along a segment z + t h in D, with r = sc_norm B z h: r^2 / (1 + t r)^2 <= D^2 B(z + t h)[h,h], and D^2 B(z + t h)[h,h] <= r^2 / (1 - t r)^2 when t r < 1. The one-dimensional comparison behind it compares 1 / sqrt (psi + e) with t for a function psi >= 0 with psi'^2 <= 4 psi^3. | ||
The Dikin ellipsoid: if sc_norm B z h < 1 then z + h is in D (Nesterov-Nemirovskii, Theorem 2.1.1); proved from the bound above and the blow-up of B at the exit point of the segment. | ||
Lemma 2.15 of Koehler and Sohn: r - ln (1 + r) <= bregman_div B (z + h) z when z + h is in D, and bregman_div B (z + h) z <= - r - ln (1 - r) when r < 1; hence (i) if the Bregman divergence is at most 1/2 - ln (3/2) then r <= 1/2 and it is at least r^2 / 3, and (ii) if r <= 1/2 then z + h is in D and |B (z + h) - B z - D B(z)[h] - r^2 / 2| <= 2 r^3 / 3. | ||
A self-concordant function is convex on D, and continuous at every point of D for the points of D. | ||
Lemma 2.10 of Koehler and Sohn, for a theta-self-concordant barrier with theta >= 0: D B(z)[y - z] <= theta for y, z in D (Nesterov, Theorem 4.2.4), and B ((1 - eps) x + eps x0) <= B x0 + theta ln (1 / eps) for x0, x in D and 0 < eps < 1. | ||
Monotonicity on [a, b] from the sign of the derivative, and a function with a nonnegative second derivative on [a, b] lies above its tangents there. | ||
If B agrees on D, along the line through z in the direction h of V, with a function of one variable that has three derivatives, these are the derivatives of B along h at the points of the line in D. A linear form on row vectors is mxdot g h and a bilinear form Q has Q h h = h M h^T, for the vector and the matrix of their values on the basis. | ||
| logdet_ | Matrices as row vectors through mxvec: pd_slice n s is the set of the positive definite n x n matrices of trace s, logdet_barrier n x = - ln det (vec_mx x), pd_slice2 n m M is the set of the matrices A of trace n with m I < A < M I, logdet_barrier2 n m M x = - ln det (A - m I) - ln det (M I - A) + n ln ((1 - m) (M - 1)), and sym_traceless n is the subspace of the symmetric matrices of trace 0. | |
For A positive definite and U symmetric there are G invertible and reals l_i with A = G^T G and U = G^T diag(l) G; hence -ln det (A + t U) = c - sum_i ln (1 + t l_i) whenever A + t U is positive definite, which happens exactly when every 1 + t l_i is positive, and tr (A^-1 U) = sum_i l_i, tr ((A^-1 U)^2) = sum_i l_i^2. | ||
A function that equals c - sum_(i < k) ln (1 + t l_i) along every line through D (with D convex and relatively open, the l_i and c depending on the line), and whose first and second derivatives at each point of D are a linear and a bilinear form, is a k-self-concordant barrier on D. | ||
Lemma 2.8 of Koehler and Sohn, one-sided (Nesterov-Nemirovskii, Proposition 5.4.5): pd_slice n s is convex and relatively open with directions sym_traceless n, and logdet_barrier n is an n-self-concordant barrier on it. On pd_slice n n it is nonnegative (det A <= (tr A / n)^n), with value 0 at the identity. | ||
Lemma 2.8 of Koehler and Sohn, two-sided: pd_slice2 n m M is convex and relatively open with directions sym_traceless n, and logdet_barrier2 n m M is a 2n-self-concordant barrier on it; if m < 1 < M it is nonnegative there, with value 0 at the identity. | ||
| least_ | The least squares objective with a selection P of the features and a weight s: s sum_(i in P) (b - <Z_i, theta>)^2 + beta (lambda |theta|^2 + b^2) + gamma B theta; with P the indices other than i and s = 1 / (2 n) it is the leave-one-out objective of the Lindeberg argument. | |
| minimizers.v | Every subspace V of 'rV[R]_N is the row space of a matrix with \dim V orthonormal rows, and is closed; for D convex and relatively open with directions V, z in D and y in the closure of D, y - z is in V and z + t (y - z) is in D for 0 <= t < 1. | |
For B >= 0 a self-concordant function on D and g continuous, convex on D and nonnegative, the sublevel sets of g + gamma B in D are closed, and if g z >= kappa |z|^2 with kappa > 0 then g + gamma B attains its minimum on D (D need not be bounded). In particular the least squares objective with a barrier attains its minimum on D x R. | ||
At a minimizer (theta, b) the derivative along every direction of V x R is 0, and F (theta + h) (b + c) - F theta b is the quadratic part at (h, c) plus gamma times the Bregman divergence of B (Koehler-Sohn, (2.17)-(2.18)). For H positive definite, the infimum over u of u H u^T / 2 + (r + <a, u>)^2 / (2 nn) is r^2 / (2 (nn + l)) with l = a H^-1 a^T ((2.19)). | ||
| ls_ | Lemmas 4.1 and 4.2 and Proposition 2.14, (2.23), pointwise: for the leave-one-out minimizer of the barrier-regularized problem, the Hessian H in coordinates of V x R is positive definite; the cost Delta(z) of inserting a feature z satisfies 0 <= Delta(z) <= r(z)^2 / (2 n), and if 36 <= n gamma then |Delta(z) - r(z)^2 / (2 (n + l(z)))| <= (2 + 3 r(z)^4) / (n sqrt (n gamma)), with r(z) the residual of z and l(z) = <alpha(z), H^-1 alpha(z)>. | |
l(z) = c0 - 2 <v, z> + z T z^T with T symmetric, 0 <= c0 <= 1 / (2 beta), |v|^2 <= k / (4 beta^2 lambda), 0 <= z T z^T <= |z|^2 / (2 beta lambda) and |T|_F^2 <= k / (4 beta^2 lambda^2), k = \dim V; and (2.21): beta (lambda |theta_m|^2 + b_m^2) is at most the leave-one-out objective at (theta_ref, 0). | ||
| feature_ | For a (K, tau)-regular feature mu with covariance Sigma (Koehler-Sohn, Definition 2.5): every measurable g with |g z| <= a + b |z|^4 is integrable, E <z, theta> = 0, E <z, theta> <z, theta'> = theta Sigma theta'^T, E z T z^T depends only on Sigma and T, and E (z T z^T - E z T z^T)^2 <= tau^2 |T|_F^2 for T symmetric. | |
E (b - <z, theta>)^2 = b^2 + theta Sigma theta^T, E (b - <z, theta>)^4 <= 8 (1 + K^4) (lambda |theta|^2 + b^2)^2 with lambda = opnorm Sigma, and for l z = c - 2 <z, v> + z T z^T with T symmetric, E l = c + E z T z^T and E (l - E l)^2 <= 2 tau^2 |T|_F^2 + 8 lambda |v|^2; v Sigma v^T <= opnorm Sigma |v|^2. | ||
| gauss_ | For x of law gauss k and A symmetric, E x A x^T = tr A and E (x A x^T)^2 = (tr A)^2 + 2 |A|_F^2 (spectral theorem and orthogonal invariance of gauss k); E <x, a> = 0, E <x, a> <x, b> = <a, b> and E <x, a>^4 = 3 |a|^4. | |
(2.10) of Koehler and Sohn: for S != 0 and a law nu on 'rV[R]_N with nu A = gauss k [set x | A (x S)], nu is a (3^(1/4), sqrt 2 opnorm (S^T S))-regular feature with covariance S^T S; opnorm S ^ 2 <= opnorm (S^T S). | ||
| barrier_ | Lemma 2.11 of Koehler and Sohn: for B >= 0 a theta-self-concordant barrier on D (convex, relatively open), theta_ref in D, lambda, beta >= 0, gamma > 0 and 0 < eps < 1, 0 <= Phi_Z(D, B; beta, gamma) - Phi_Z(D; beta) <= eps F_Z(theta_ref, b_ref; beta) + gamma B theta_ref + gamma theta ln (1 / eps) for every tuple of features Z, by contracting toward the reference point (F_Z is convex); hence (2.15), the comparison of the values without barrier for two tuples W and G. | |
| barrier_ | The value Phi_Z(D, B; beta, gamma) of the barrier-regularized problem is a measurable function of the features Z, for D convex and relatively open and B >= 0 continuous on D: an infimum over D of an upper semicontinuous family is the infimum over a countable dense subset. | |
Lindeberg's replacement for a nonnegative integrable functional F of n independent coordinates, with bounds b_i that may depend on the other coordinates: if |E_mu F(x^(i <- t)) - E_nu F(x^(i <- t))| <= b_i x for all i and x, then |E_(mu^n) F - E_(nu^n) F| <= sum_i E b_i under the hybrid law with mu before i and nu after. The integral of a function that does not depend on a coordinate does not depend on its law, and the coordinate j of tuple_prod rho n has law rho j. | ||
Propositions 2.14 and 2.16 of Koehler and Sohn: for two regular features with the same covariance, the means of the cost of inserting one feature differ by at most (4 + 48 (1 + K^4) S^2) / (n sqrt (n gamma)) + 4 sqrt (1 + K^4) sqrt (dim V) (tau / lambda + 1) S / (beta n^2), where S = lambda |theta_m|^2 + b_m^2 is the size of the leave-one-out minimizer; for the value itself the same holds with S replaced by its bound ((2 n)^-1 sum_(j <> i) <x_j, theta_ref>^2 + beta lambda |theta_ref|^2 + gamma B theta_ref) / beta, and the variance in the coordinate i is at most 2 (1 + K^4) / n^2 times the square of that bound. | ||
Theorem 2.9 of Koehler and Sohn, for mu, nu (K, tau)-regular with the same covariance, D convex, relatively open and nonempty (not necessarily bounded), B >= 0 self-concordant on D, beta, gamma > 0 and Lref = (1 + 1/beta) (1 + inf_D (lambda |theta|^2 + gamma B theta)): if 36 <= n gamma, |E_(mu^n) Phi - E_(nu^n) Phi| <= 100 (1 + K^4)^2 Lref^2 ((n gamma)^(-1/2) + sqrt (dim V) (tau / lambda + 1) / n); Var_(mu^n) Phi <= 4 (1 + K^4)^2 Lref^2 / n; and Phi is within that bound plus t of E_(nu^n) Phi outside an event of mu^n-probability at most 4 (1 + K^4)^2 Lref^2 / (n t^2). | ||
| ridge_ | The comparison of ridge-regularized least squares values of Koehler and Sohn (proposition at lines 6365-6416), as a concentration inequality with the barrier weight gamma and the contraction eps left free: for mu, nu (K, tau)-regular with the same covariance, B >= 0 a theta-self-concordant barrier on D, theta_0 in D, t, M > 0 and 36 <= n gamma, the mu^n-probability that |Phi_Z(D; beta) - E_(nu^n) Phi_Z(D, B; beta, gamma)| exceeds the bound of (2.12) plus t + eps M + gamma B theta_0 + gamma theta ln (1 / eps) is at most 4 (1 + K^4)^2 Lref^2 / (n t^2) + (theta_0 Sigma theta_0^T / 2 + beta lambda |theta_0|^2) / M (Theorem 2.9, Lemma 2.11 and Markov's inequality for F_Z(theta_0, 0; beta), whose mean is the last numerator). | |
Phi_Z(D; beta) is the value with a barrier of weight 0, hence a measurable function of the features for D convex, relatively open and nonempty; Markov's inequality P(f > M) <= E f / M for f >= 0 integrable. | ||
| moreau.v | Projections in 'rV[R]_N with the Frobenius inner product: a nonempty closed set has a nearest point to every z (compactness of the closed bounded sets); for K closed, convex and nonempty, p in K is nearest to z iff <z - p, y - p> <= 0 for every y in K, the nearest point proj K z is unique, and |proj K z - proj K z'| <= |z - z'|. | |
Lemma 5.1 of Koehler and Sohn (Moreau's decomposition): for a closed convex cone C, z = proj C z + proj (polar C) z with the two parts orthogonal, so |z|^2 = |proj C z|^2 + |proj (polar C) z|^2; p in C is proj C z iff z - p is in the polar cone and orthogonal to p; and sup_(y in C, |y| <= 1) <z, y> = |proj C z|. | ||
| feature_ | Under a law on 'rV[R]_N with E <z, theta>^4 <= A |theta|^4 for every theta, a measurable g with |g z| <= a + b |z|^4 for every z (a bound on the absolute value) is integrable, so the linear forms, their products and the quadratic forms z T z^T are integrable and z T z^T is square integrable; if moreover E <z, theta> <z, theta'> = theta Sig theta'^T, then E z T z^T = <Sig^T, T>. | |
A finite mixture of laws P i on 'rV[R]_N, each centered with second-moment matrix Sig i, E_i <z, theta>^4 <= A |theta|^4 and Var_i (z T z^T) <= tau^2 |T|_F^2 for T symmetric, is a regular feature with covariance Sigma = sum_i w_i Sig i, any K with A <= K^4 opnorm Sigma^2, and sqrt (tau^2 + c^2) in place of tau, when opnorm Sigma > 0 and sum_i w_i <Sig i - Sigma, T>^2 <= c^2 |T|_F^2 for every symmetric T (the law of total variance, with E_i z T z^T - E z T z^T = <Sig i - Sigma, T> for T symmetric). | ||
The same when opnorm Sigma > 0 and sum_i w_i |Sig i - Sigma|_F^2 <= c^2, which implies the hypothesis of mixture_regular_feature_dot by Cauchy-Schwarz for the Frobenius product; no structure of Sig i - Sigma is needed. |
random_matrix/25 rows
| 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. |
applications/18 rows
| File | Results | Statement |
|---|---|---|
| MatrixSeriesTheorem.v | Proves matrix_series_statement (T1). (a) For symmetric H_1, ..., H_r in 'M[R]_n, S = \sum_j H_j H_j and g of law gauss r, E tr (\sum_j g_j H_j)^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S for every q >= 1 (gauss_mx_series_moment). (b) For B_1, ..., B_r in 'M[R]_(m, p) and every q >= 1, E opnorm (\sum_j g_j B_j) <= ((2q - 1)!! sigma^(2(q-1)) tau)^(1/(2q)), 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) (gauss_mx_series_opnorm). (c) With C = 5: if sigma^2 <= sqrt d and tau <= 2 d for a real d >= 1, then E opnorm (\sum_j g_j B_j) <= 5 sqrt (sqrt d) sqrt (ln (2 + d)) (gauss_mx_series_opnorm_log). The expectations are integrals in the extended reals. Axioms: three of boolp. | |
| TensorPackingTheorem.v | Proves tensor_packing_statement (T2) with C = 30000: for every R : realType, 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, the number of indices a with sum_k (x_a A_k y_a^T)^2 >= eps^2 is at most 30000 (1 + L) / eps^2 exp (30000 eps^(-2) sqrt d ln (2 + d)), from tensor_packing of library/. Axioms: three of boolp. | |
| GoeEdgeTheorem.v | Proves goe_edge_statement (T3): for every R : realType, d >= 1, a of law gauss (d * d) and W = goe_mx a, the map a |-> lambda_max W is measurable and integrable, E lambda_max W <= 2, P(lambda_max W >= 2 + t) and P(lambda_max (- W) >= 2 + t) are at most exp (- d t^2 / 4), and P(opnorm W >= 2 + t) <= 2 exp (- d t^2 / 4), for every t >= 0. From library/. | |
| PsdSplittingTheorem.v | 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/. | |
| Perceptron/Pressure.v | For N >= 1 and f with three derivatives such that |f| <= B0, |f'| <= B1, |f''| <= B2 and |f'''| <= B3: the pressure p_N(G, f) is at most M B0 in absolute value and measurable in the entries of G; along each entry of G it has three derivatives, the third at most (B3 + 6 B1 B2 + 6 B1^3) / (N^2 sqrt N) in absolute value (from log_partition_derive3); and g |-> p_N(vec_mx g, f) is integrable against gauss (M * N) with |E_sign p_N - E_Gauss p_N| <= (B3 + 6 B1 B2 + 6 B1^3) / 2 M N^(-3/2) (from rademacher_gauss_lindeberg over the M N entries). | |
| PerceptronSignTheorem.v | Proves perceptron_sign_statement (T6) with C = 1 + (|B3| + 6 |B1| |B2| + 6 |B1|^3) / 2, from perceptron_sign_compare of Perceptron/. The continuity of f''' required by bounded_C3 is not used. Axioms: three of boolp. | |
| SKGap/Ising.v | For the Ising law nu of a matrix A and a field theta on {-1, 1}^n (the definitions of T4), the conditional expectation E_i given the spins outside i and D_i = I - E_i satisfy D_i f = (x_i - m_i) d_i f, nu[(D_i f)^2] = nu[v_i (d_i f)^2] and nu[g D_i f] = nu[D_i g D_i f]; the Dirichlet form vanishes only on the constants; ising_gen f = sum_i D_i f. For A symmetric with zero diagonal and i != j, the weights of the four configurations of the spins i and j, the other spins fixed, are K (1 + a x)(1 + b y)(1 + t x y) with K > 0, |a|, |b| < 1 and t = tanh A_ij. |tanh u| <= |u| and |tanh u - u| <= |u|^3. | |
| SKGap/Disorder.v | The good-disorder event of T4 (item T4b), for beta >= 0 and a fixed delta > 0: sk_good_disorder n beta delta is the set of the a of 'rV[R]_(n * n) whose coupling J = sk_coupling beta a satisfies opnorm J <= 2 beta + delta, sum_j J_ij^2 <= beta^2 + delta for every i and |J_ij| <= delta for every i and j. It is measurable, and for every eps > 0 there is N such that its probability under gauss (n * n) is at least 1 - eps for every n >= N. The proposition 'Good disorder' of the manuscript, with delta fixed instead of n^(-1/4), from goe_opnorm_edge_tail and the tails of random_matrix/. R is implicit; the other arguments are explicit. | |
| SKGap/Spectral.v | The spectral step of T4 (item T4a). For any matrix A, field theta and real k: if k E(g) <= nu[(L g)^2] for every g, where nu is the Ising law, E = ising_dirichlet A theta and L = ising_gen A theta = sum_i D_i, then k Var_nu(f) <= E(f) for every f. In L^2(nu), L is linear and self-adjoint, <f, L f>_nu = E(f), and the kernel of L is the constants, so wpoincare_from_square of probability/ applies. R, n, A, theta and k are implicit. | |
| SKGap/TwoSpin.v | The uniform two-spin inequality. For the pair law proportional to (1 + a x)(1 + b y)(1 + t x y) with |a|, |b| <= 1 and |t| <= 1/1000: the mixed energy plus the correction term (t + 2 t^2 m_i m_j) v_i v_j d_i f d_j f is at least - 70000 |t|^3 times the sum of the two energies (pair_two_spin; the remainder in t by a real polynomial certificate, ts_coef_bound). For the Ising law of a symmetric A with zero diagonal and i != j with |tanh A_ij| <= 1/1000: nu[D_i f D_j f] >= - nu[(t + 2 t^2 m_i m_j) v_i v_j d_i f d_j f] - 70000 |t|^3 (nu[v_i (d_i f)^2] + nu[v_j (d_j f)^2]) with t = tanh A_ij (ising_two_spin). | |
| SKGap/Poincare.v | For A symmetric with zero diagonal, |tanh A_ij| <= 1/1000, opnorm (tanh A_ij) <= M, 2 opnorm (tanh^2 A_ij) <= M and sum_j |tanh A_ij|^3 <= rho for every row: nu[(sum_i D_i f)^2] >= (1 - M - 140000 rho) E(f). For k > 0, from k Var_nu(f) <= E(f) for all f: opnorm Cov_nu(x) <= 1 / k. The deterministic gap: for 0 <= beta < 1/2, 0 < delta <= sk_gap_tol beta = min (1/2000) ((1 - 2 beta)/400000), J symmetric with zero diagonal, opnorm J <= 2 beta + delta, sum_j J_ij^2 <= beta^2 + delta and |J_ij| <= delta, and 0 <= s <= 1: kappa Var_nu(f) <= E(f) for every f and opnorm Cov_nu(x) <= 1 / kappa, kappa = (1 - 2 beta)/2, for the Ising law of s J and any field. | |
| RandomSAT/Model.v | For a tuple t of M clauses, the largest satisfiable prefix length sat_prefix_len t, the cap M included, is the lifetime life [set: _] t: the number of nonempty solution sets among those of the nonempty prefixes of t. #|clause n k| = 'C(n, k) 2^k. For k <= n, the uniform mean over clause n.+1 k.+1 is the mixture, with weights 1 - k.+1/n.+1 and k.+1/n.+1, of the clauses without the first variable (a uniform clause of size k.+1 on the other n variables) and of the clauses with it (a uniform sign and a uniform clause of size k on the others). | |
| RandomSAT/Pivotal.v | For k <= n, a set S of assignments on n variables and m <= M, the variance of the lifetime life S t of m independent uniform clauses t of size k is at most 2 m times the sum over j < m of the mean of min(M q_j, 1), where q_j is the probability that one more clause empties the solution set of the first j clauses. | |
| RandomSAT/Replacement.v | For a nonempty set S of assignments on n variables with b forced variables (on which all its elements agree), the probability that a uniform clause of size k empties S is 'C(b, k) / ('C(n, k) 2^k). For 1 <= r < v, a > 0 with 1 / (v + 1) <= a^-r and an integer g >= 2 (r + 1) a, a block of g independent uniform clauses of size r + 1 empties a set S of assignments on v variables with probability at least kill r S - a^-r, for every S. | |
| RandomSAT/Forcing.v | For 1 <= k < n, a > 0 with 1 / (n + 1) <= a^-k, an integer g >= 2 (k + 1) a and p = (k + 1) / (n + 1), the probabilities h_j that the first variable is forced by j independent uniform clauses of size k + 1 on n + 1 variables satisfy sum_(j <= M) h_j <= g M p + (M + 1) M p a^-k for every M. The mean fraction of forced variables after j clauses is h_j. | |
| RandomSAT/Variance.v | sat_capped_var R n k is the variance of the lifetime of the set of all assignments over sat_cap k n clauses. For 0 < k <= n, c >= 0 and M <= c^k, min(M q, 1) <= c b / n, where q is the probability that a uniform clause of size k empties a set of assignments with b forced variables. sat_variance_bound_explicit: for K >= 3 and N >= K + 1, sat_capped_var R N K <= 8 4^(K+1) K (3 K + 2^(K+2)) N^(1 + 2/K); sat_variance_bound is its existential form, the form of the statement. | |
| SatVarianceTheorem.v | Proves sat_variance_statement (T7), with the constant C = 8 4^(k+1) k (3 k + 2^(k+2)) of sat_variance_bound_explicit: for every R : realType, k >= 3 and n >= k + 1, the variance sat_capped_var R n k of the largest satisfiable prefix length, capped at 2^(k+1) n, of 2^(k+1) n independent uniform proper signed k-clauses on n variables is at most C n^(1 + 2/k) (powR). From sat_variance_bound of RandomSAT/. Axioms: three of boolp. | |
| SKGapTheorem.v | Proves sk_gap_statement (T4) with the events E_n = sk_good_disorder n beta (sk_gap_tol beta) of SKGap/: measurable, of probability tending to one under gauss (n * n), and on them, for every n, s in [0, 1] and field theta, (1 - 2 beta)/2 Var_nu(f) <= E(f) for every f and opnorm Cov_nu(x) <= 2 / (1 - 2 beta). Axioms: three of boolp. |