On this page
GaussianAnalysisprobability/
probability/
Paley-Zygmund and other moment inequalities, the Lindeberg replacement method, subgaussian and subexponential variables (Hoeffding, Bernstein, Hanson-Wright), the norms of random vectors and matrices with subgaussian coordinates, the Efron-Stein inequality, product laws by rows and conditioning on coordinates, measurable choices of minimizers, symmetrization and the small-ball method, the semicircle law and the scalar variational problem of the Gaussian model, and its version over clipped profiles with its dual form, the omission form of the Efron-Stein 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 holds the library's general probability tools, mostly built on tuple_prod, the law of n independent random elements with laws mu 0, ..., mu (n - 1). Independent variables are functions f_i (x_i) of the coordinates of a tuple x of this law.
Some files prove classical nonasymptotic inequalities, with explicit constants: Paley-Zygmund, Efron-Stein, Hoeffding, Bernstein, Hanson-Wright, symmetrization and the small-ball method. Others treat mixtures, total variation, densities, the semicircle law, the scalar variational problem of Koehler and Sohn and, in general form, steps of the manuscripts of applications/.
Reading order
lindeberg.v:tuple_prodand Lindeberg's replacement principle.tuple_rows.v: Fubini, independent rows and blocks, coordinatewise images.moments.v: the Paley-Zygmund inequality.conditioning.v: resampling coordinates outside a set; independence of events on disjoint coordinates.efron_stein.v: the Efron-Stein inequality.efron_stein_omission.v: its omission form, due to Steele.subgaussian.v: subgaussian and subexponential variables, Hoeffding's and Bernstein's inequalities.subgaussian_matrix.v: norms of random vectors and matrices with subgaussian entries.hanson_wright.v: the Hanson-Wright inequality.mixture.v: finite mixtures and independent draws from them.countable_mixture.v: countable mixtures, independent draws, and a coupling with finite mixtures.total_variation.v: the total variation distance.atoms.v: atoms of finite measures; null sets of products.density_law.v: laws with a density against a probability.symmetrization.v: Rademacher averages, contraction and symmetrization.small_ball_method.v: Mendelson's small-ball method.measurable_minimizer.v: measurable choice of minimizers.variational.v: the scalar variational problem of Koehler and Sohn.clip_profile.v: a constrained version, solved by clipped profiles, with a dual form.semicircle_law.v: the semicircle law and its moments.finite_mean.v: uniform means and variances on finite types.finite_gap.v: Poincare inequalities on finite weighted spaces.log_partition.v: derivatives of log-partition functions.rademacher_lindeberg.v: replacing uniform signs by Gaussians.
Core definitions
tuple_prod(lindeberg.v): tuple_prod mu n, the product of mu 0, ..., mu (n - 1) on n-tuples, by recursion on n.tuple_set(lindeberg.v): x with coordinate i replaced by t.tuple_merge(conditioning.v): the coordinates of x in S and of y outside S. An event E depends only on S when E (tuple_merge S x y) = E x for all x, y.subgaussian,subexponential(subgaussian.v): X measurable, K > 0 and E exp(X^2 / K^2) <= 2, respectively L > 0 and E exp(|X| / L) <= 2.mixture,cmixture(mixture.v,countable_mixture.v): A |-> sum_i w_i P_i(A), for weights w_i >= 0 of sum one.density_law(density_law.v): A |-> int_A f dmu, for f measurable, nonnegative and of integral one (prob_density).rademacher_mean(symmetrization.v): the average over the 2^n sign vectors.upper_moment,upper_cutoff,upper_value(variational.v): m(w) = E max(X - w, 0) and s(w) = E max(X - w, 0)^2, the cutoff sup {v | v + z <= c m(v)}, and s + c m^2 there.
Main results
Product laws.
lindeberg_replacement: for F bounded and measurable on n-tuples, if replacing mu i by nu i at coordinate i moves the integral of F by at most B i whatever the other coordinates, the integrals of F under the two product laws differ by at most sum_i B i.tuple_prod_tvapplies it to indicators of measurable sets, with B i = tv_dist (mu i) (nu i).efron_stein: Var F <= sum_i E Var_i F for F square integrable, Var_i being the variance in coordinate i, the others fixed.efron_stein_omission: Var F <= sum_i E (G_i - F)^2 for F integrable and measurable G_i not depending on coordinate i.
Concentration (X_i = f_i (x_i), centered).
subgaussian_sum(Hoeffding): if X_i is subgaussian with constant K_i and S = sum_i a_i^2 K_i^2 > 0, then sum_i a_i X_i is subgaussian with constant 4 sqrt S.bernstein(subgaussian.v): if X_i is subexponential with constant L_i, then P(|sum_i a_i X_i| >= t) <= 2 exp(-min(t^2 / (64 sum_i a_i^2 L_i^2), t / (4 max_i |a_i| L_i))) for t >= 0.hanson_wright: if every X_i is subgaussian with constant K, then for an n x n matrix A, Q = sum_(i,j) a_ij X_i X_j has P(|Q - sum_i a_ii E X_i^2| >= u) <= 2 exp(-min(u^2 / (6912 K^4 |A|_F^2), u / (136 K^2 opnorm A))) for u >= 0.subgaussian_opnorm_tail: for an m x n matrix of such entries and t >= 0, P(opnorm > 21 K (sqrt m + sqrt n + t)) <= 2 exp(-t^2).
Empirical processes.
small_ball_method: let n, u, q > 0 and measurable f_j with mu_k(|f_j| >= 2 u) >= q for all j and k < n. If the expected Rademacher average of max_(j < J) |(1/n) sum_k eps_k f_j(x_k)| is at most r for every J, the event that some f_j has sum_k f_j(x_k)^2 < n u^2 q / 2 has probability at most 8 r / (u q).
Mixtures and variational problems.
tuple_prod_mixture,tuple_prod_cmixture: n independent draws from a finite or countable mixture are the mixture, over label tuples s, of the products of the P (s_k), with weights prod_k w (s_k).upper_variational: for a law on the line with E X^2 < +oo and c > -1, the supremum of max(E (X + z) f(X), 0)^2 / (E f(X)^2 + c (E f(X))^2) over measurable f >= 0 with f^2 integrable and E f > 0 is s(w) + c m(w)^2, where w is the unique root of w + z = c m(w) (upper_cutoff_unique).
Tools of applications/.
wpoincare_from_square: let w be positive weights of sum one, and L linear, self-adjoint and nonnegative in L^2(w), with the constants as kernel. If k (f, L f)_w <= (L f, L f)_w for every f, then k Var_w(f) <= (f, L f)_w.rademacher_gauss_lindeberg: for F bounded and measurable on row vectors of length n, with third derivative along coordinate j at most c_j in absolute value, the average of F over the 2^n sign vectors and its integral under gauss n differ by at most (1/2) sum_j c_j.
How the proofs go
hanson_wrightdecouples the off-diagonal part over sets of coordinates (offdiag_decouple) and applies Hoeffding twice with a Gaussian chaos bound; the diagonal uses Bernstein.small_ball_methodusessymmetrization,contractionand Markov's inequality, without a concentration inequality.rademacher_gauss_lindebergreplaces one coordinate at a time, with Taylor's formula of order two.
Connections
Outside the directory, some files require gaussian/, comparison/, matrix/ and, for measurable_minimizer.v, convex/. It is used by comparison/, matrix/, convex/, fourier/ (only lindeberg.v), random_matrix/ (wigner.v, restricted_isometry.v) and applications/: T4 uses finite_gap.v, T6 log_partition.v and rademacher_lindeberg.v, and T7 finite_mean.v. The extension/ proofs use it widely, and theories/ uses moments.v.
Files
| File | Title | Lines | Lemmas | Defs | Requires in this directory |
|---|---|---|---|---|---|
| moments.v | Moment inequalities | 156 | 7 | 0 | none |
| lindeberg.v | The Lindeberg replacement method | 303 | 17 | 3 | none |
| subgaussian.v | Subgaussian and subexponential random variables | 967 | 31 | 3 | lindeberg, tuple_rows |
| subgaussian_matrix.v | Norms of random vectors and matrices with subgaussian coordinates | 538 | 7 | 0 | lindeberg, subgaussian |
| mixture.v | Finite mixtures of probabilities | 400 | 18 | 2 | lindeberg, moments, conditioning, subgaussian |
| countable_mixture.v | Countable mixtures of probabilities | 669 | 17 | 5 | lindeberg, conditioning, mixture |
| total_variation.v | The total variation distance | 264 | 18 | 1 | lindeberg |
| atoms.v | Atoms of a finite measure | 197 | 5 | 1 | none |
| efron_stein.v | The Efron-Stein inequality and moment bounds for product laws | 1,005 | 35 | 0 | lindeberg, tuple_rows, moments |
| efron_stein_omission.v | The omission form of the Efron-Stein inequality | 106 | 2 | 0 | lindeberg, efron_stein |
| finite_mean.v | Uniform means on finite types | 313 | 32 | 2 | none |
| tuple_rows.v | Product laws by blocks | 498 | 21 | 3 | lindeberg |
| semicircle_law.v | The semicircle law | 813 | 31 | 2 | none |
| variational.v | A scalar variational problem for a law on the line | 1,764 | 80 | 11 | none |
| clip_profile.v | Clipped profiles: a constrained scalar variational problem | 1,080 | 48 | 6 | variational |
| symmetrization.v | Rademacher averages, contraction and symmetrization | 866 | 42 | 8 | lindeberg, tuple_rows, efron_stein |
| small_ball_method.v | The small-ball method | 820 | 20 | 2 | lindeberg, moments, symmetrization, efron_stein |
| conditioning.v | Conditioning a product law on a set of coordinates | 521 | 20 | 4 | lindeberg, tuple_rows |
| density_law.v | Laws given by a density | 426 | 20 | 3 | lindeberg, tuple_rows, conditioning |
| hanson_wright.v | The Hanson-Wright inequality | 985 | 26 | 9 | lindeberg, subgaussian, conditioning |
| measurable_minimizer.v | Measurable minimizers | 395 | 21 | 3 | lindeberg |
| log_partition.v | Derivatives of a log-partition function | 215 | 8 | 1 | none |
| rademacher_lindeberg.v | Lindeberg's replacement of uniform signs by Gaussians | 523 | 15 | 2 | lindeberg |
| finite_gap.v | Spectral gaps on a finite space | 256 | 16 | 5 | none |
Table of main results71 rows of the README
| 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. |