On this page
GaussianAnalysiscomparison/
comparison/
Linear images and rotation invariance, shifts, tails, moment generating functions and chi-square laws, concentration of Lipschitz functions and the Poincare inequality, Slepian, Sudakov-Fernique and Gordon comparison inequalities, Sudakov's minoration, escape through a mesh, norms of Gaussian matrices, the convex Gaussian min-max theorem, the Ornstein-Uhlenbeck semigroup and the Brascamp-Lieb inequality.
Guide
Written for this documentation from the sources and the README, and checked against the Rocq statements. The file headers and the statements are the reference.
This directory proves the classical inequalities for Gaussian vectors: linear images, rotations, shifts, tails, concentration of Lipschitz functions, the comparisons of Slepian, Sudakov-Fernique and Gordon, and Sudakov's minoration. It applies them to Gaussian matrices up to the convex Gaussian min-max theorem (CGMT), and ends with the Ornstein-Uhlenbeck semigroup and the Brascamp-Lieb inequality. Random matrix, Fourier and subgaussian files of the library build on it.
The files rest on gauss n, the standard Gaussian measure on 'rV[R]_n (gaussian/), and on the normal laws normal_prob m s of MathComp-Analysis. Below, x and y have laws gauss n and gauss m, so x *m A is centered Gaussian with covariance A^T A; G = vec_mx a, a of law gauss (N * M), is an N x M matrix of independent standard normal entries; g and h are independent with laws gauss N and gauss M. |x| is the Euclidean norm frobenius x, <x, y> is mxdot, and F is L-Lipschitz when |F x - F y| <= L |x - y|.
Reading order
normal_mgf.v: exponential moments and tails of normal_prob m s; Chernoff's bound.normal_linear.v: affine images of Lebesgue measure and normal laws; linear combinations of two independent normal variables.chi_square.v: exponential moments and tails of weighted centered chi-square sums.gauss_linear.v: law and tails of a linear form <x, a>.gauss_rotation.v: rotation invariance of two independent standard Gaussian vectors.gauss_shift.v: the Cameron-Martin formula.gauss_smoothing.v: Gaussian smoothing of bounded Lipschitz functions.gauss_concentration.v: concentration and the Poincare inequality for Lipschitz functions.slepian.v: the Sudakov-Fernique and Slepian inequalities.gordon.v: Gordon's min-max inequality.gauss_law.v: the law of x *m A depends only on A^T A.gauss_matrix_law.v: Gaussian matrices from independent Gaussian rows, and their transposes.escape.v: escape through a mesh and norms of Gaussian matrices.sudakov.v: Sudakov's minoration and the dual Sudakov inequality.cgmt.v: the CGMT in mean and concentration form.cone_escape.v: the CGMT on cones.ornstein_uhlenbeck.v: the Mehler transform and Ornstein-Uhlenbeck semigroup.brascamp_lieb.v: the Gaussian Brascamp-Lieb inequality for functions with values in [delta, K].brascamp_lieb_lebesgue.v: the extension to [0, +oo]-valued functions and the Lebesgue form.
Core definitions
gauss_smooth(gauss_smoothing.v): x |-> E[G (x + eps y)], y of law gauss n.rmaxandincr_var(slepian.v): the largest coordinate of a row vector; the variance of (x *m A)_j - (x *m A)_l, computed from A^T A.minmax(gordon.v): the smallest of the row maxima of a matrix.gwidth_funandescape_inf(escape.v): sup_(x in T) <h, x>, whose mean is the Gaussian width of T, and inf_(x in T) |G x|.cgmt_aux(cgmt.v): inf_(x in K) (|g| |x| - <h, x>)_+, the auxiliary value of the CGMT.cone_sup(cone_escape.v): sup_(x in K, |x| <= 1) <h, x>.mehlerandou(ornstein_uhlenbeck.v): mehler r f x = E[f (r x + sqrt (1 - r^2) Z)], Z standard normal; ou t f = mehler (exp (- t)) f.
Main results
The normal law.
integral_normal_expR,normal_prob_abs_tail: for X of law normal_prob m s, s != 0, E exp(t X) = exp(t m + t^2 s^2 / 2), and P(|X - m| >= u) <= 2 exp(- u^2 / (2 s^2)) for u >= 0.normal_prob_lincomb: for independent X, Y of laws normal_prob m1 s1 and normal_prob m2 s2, with s1, s2, b nonzero, a X + b Y has law normal_prob (a m1 + b m2) (sqrt (a^2 s1^2 + b^2 s2^2)).
Gaussian vectors.
gauss_mxdot: for a != 0, <x, a> has law normal_prob 0 |a|.integral_gauss_shift: E[f (x + h)] = E[f x exp(<h, x> - |h|^2 / 2)] for measurable f with extended real values.gauss_mulmx_law,gauss_orthogonal_law: if A^T A = B^T B, x *m A and y *m B have the same law; if A^T A = 1, x *m A has law gauss k.
Concentration and comparison.
gauss_concentration,gauss_concentration_abs_tail,gauss_poincare_lipschitz: for F L-Lipschitz, E exp(t (F x - E F)) <= exp(t^2 L^2 / 2) for real t, P(|F x - E F| >= u) <= 2 exp(- u^2 / (2 L^2)) for u >= 0, and E[(F x - E F)^2] <= L^2.sudakov_fernique,slepian: if incr_var A j l <= incr_var B j l for all j, l, then E rmax (x *m A) <= E rmax (y *m B); equal variances and (B^T B)_jl <= (A^T A)_jl suffice.gordon: for X = vec_mx (x *m A) and Y = vec_mx (y *m B), if increments within a row have no larger variance in X than in Y and increments across distinct rows no smaller, E minmax X <= E minmax Y.
Gaussian matrices.
gordon_escape: for N > 0 and T a nonempty set of unit vectors of 'cV[R]_M, E inf_(x in T) |G x| >= E|g| - E gwidth_fun T h.gauss_opnorm_mean_sqrt: E opnorm G <= sqrt N + sqrt M for N, M > 0.cgmt_lower,cgmt_upper: for nonempty K in 'cV[R]_M with |x| <= rho on K, E escape_inf K G >= E cgmt_aux K g h - rho if N > 0, and E escape_inf K G <= E cgmt_aux K g h + rho if K is closed and convex.
Ornstein-Uhlenbeck and Brascamp-Lieb.
is_derive_ou_t,ou_cvg0_L1: for f measurable and bounded, d/dt ou t f = (ou t f)'' - x (ou t f)' for t > 0, and ou t f -> f in L^1 of the standard normal law as t -> 0+.gauss_brascamp_lieb_bounded: for unit vectors u_i of 'rV[R]_m, 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).gauss_brascamp_lieballows measurable F_i : R -> [0, +oo], andbrascamp_liebis the Lebesgue form.
How the proofs go
- Concentration follows Herbst. For F bounded and C^1 with gradient norm at most L, rotation against an independent copy and integration by parts give
gauss_herbst_ineq, then a differential inequality for E exp(t F). Clipping, smoothing and Fatou's lemma reach every Lipschitz F. sudakov_ferniqueandgordonapply Kahane's inequalitygauss_comparison(gaussian/) to the smooth maximumlseb and the soft min-maxsmmb, and let b grow.gauss_law_smoothappliesgauss_comparison_partialin both directions to C^2 tests; double smoothing (gauss_law_lipschitz) andmeasure_lipschitz_uniquethen givegauss_mulmx_law.escape.vappliesgordonandsudakov_ferniqueto y^T G x and <g, y> + <h, x> on finite families of unit vectors, then passes to T with nets.- For Brascamp-Lieb, Lambda(r) = int exp (sum_i c_i ln (mehler r f_i)(<x, u_i>)) dgauss_m is the right side at r = 0 and the left side at r = 1. The generator identity,
gauss_ibp_unitandtight_frame_cauchy_schwarzgive r Lambda'(r) <= 0 on (0, 1).
Connections
- Requires gaussian/ (
gauss.v,gauss_ibp.v,gauss_interpolation.v,lebesgue_rV.vand others), matrix/ (euclidean.v,opnorm.v,nets.v,real_spectral.v), probability/ (moments.v,lindeberg.v,conditioning.v) and convex/ (moreau.v). - Used by random_matrix/ (
goe.v,goe_edge.v,goe_entries.v,goe_rotation.v,matrix_series.v,wigner.v), all six files of fourier/, matrix/ (covering.v,tensor_packing.v), probability/ (subgaussian.v,subgaussian_matrix.v,hanson_wright.v,semicircle_law.v), convex/ (gauss_feature.v), gaussian/ (lebesgue_rV.vrequiresnormal_linear.v), and applications/ throughSKGap/.Disorder.v
Files
| File | Title | Lines | Lemmas | Defs | Requires in this directory |
|---|---|---|---|---|---|
| normal_mgf.v | Exponential moments and tails of the normal law | 179 | 9 | 0 | none |
| chi_square.v | Exponential moments and tails of chi-square variables | 374 | 16 | 1 | normal_mgf |
| normal_linear.v | Linear images of normal laws | 246 | 9 | 0 | normal_mgf |
| gauss_linear.v | Linear forms of a standard Gaussian vector | 209 | 12 | 1 | normal_mgf, normal_linear |
| gauss_rotation.v | Rotation invariance of Gaussian measures | 511 | 17 | 0 | normal_linear |
| gauss_shift.v | Shifts of the standard Gaussian measure | 209 | 9 | 0 | normal_linear, gauss_linear |
| gauss_smoothing.v | Gaussian smoothing of Lipschitz functions | 476 | 15 | 2 | normal_mgf, gauss_shift |
| gauss_concentration.v | Gaussian concentration for Lipschitz functions | 1,214 | 25 | 1 | normal_mgf, gauss_rotation, gauss_smoothing |
| slepian.v | The Sudakov-Fernique and Slepian inequalities | 480 | 32 | 5 | gauss_smoothing |
| gordon.v | Gordon's min-max inequality | 787 | 50 | 8 | gauss_smoothing, slepian |
| escape.v | Escape through a mesh and norms of Gaussian matrices | 1,430 | 72 | 10 | gauss_rotation, gauss_smoothing, gauss_concentration, slepian, gordon |
| cgmt.v | The convex Gaussian min-max theorem, in mean and concentration form | 1,590 | 53 | 7 | gauss_concentration, slepian, gauss_smoothing, gordon, escape |
| cone_escape.v | The convex Gaussian min-max theorem on cones | 458 | 21 | 1 | gauss_concentration, gauss_smoothing, escape, cgmt |
| sudakov.v | Sudakov's minoration and the dual Sudakov inequality | 551 | 7 | 1 | gauss_smoothing, gauss_concentration, slepian, gauss_shift, escape |
| gauss_law.v | The law of a linear image of a Gaussian vector | 661 | 22 | 1 | gauss_smoothing, slepian |
| gauss_matrix_law.v | Gaussian matrices from Gaussian rows | 168 | 6 | 1 | none |
| ornstein_uhlenbeck.v | The Ornstein-Uhlenbeck semigroup | 1,654 | 48 | 8 | normal_mgf, normal_linear, gauss_smoothing |
| brascamp_lieb.v | The Gaussian Brascamp-Lieb inequality for bounded functions | 1,005 | 13 | 0 | gauss_linear, gauss_smoothing, gauss_law, ornstein_uhlenbeck |
| brascamp_lieb_lebesgue.v | The Brascamp-Lieb inequality: from bounded functions to [0, +oo] | 442 | 3 | 0 | gauss_linear, brascamp_lieb |
Table of main results68 rows of the README
| 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. |