On this page
The small-ball method
Imports 5 library modules and 26 external
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.probability.lindeberg
- GaussianAnalysis.probability.moments
- GaussianAnalysis.probability.symmetrization
- GaussianAnalysis.probability.efron_stein
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.matrix, mathcomp.algebra.rat, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.numfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.hoelder, mathcomp.analysis.probability_theory.probability
Required by 1 files of the paper proofs
Mendelson's small-ball method, in the form of Koltchinskii and Mendelson (2015, Theorem 2.1), cited by Koehler and Sohn (arXiv 2608.27372, lines 4764-4779): a uniform lower bound for the empirical second moments of a class of functions, from a lower bound on its small-ball probabilities and an upper bound on its Rademacher complexity. The deviation of the empirical process is controlled in expectation, by symmetrization and contraction (symmetrization.v), and then by Markov's inequality, so the probability of failure is of the order of the complexity: this suffices for limits in probability when the scale grows, and no bounded differences inequality is needed.
Main results, for x of law tuple_prod mu n with n > 0:
- small_ball_method: for a sequence of measurable f_j, u > 0 and q > 0 with mu_k(|f_j| >= 2 u) >= q for all j and k < n, and r with
E rademacher_mean (max_(j < J) |(1/n) sum_k eps_k f_j(x_k)|) <= r
for every J, the event small_ball_event n f (n u^2 q / 2), 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). It is measurable (measurable_small_ball_event). Proof: the ramp between u and 2 u, which is 1/u-Lipschitz (ramp_lipschitz), symmetrization and contraction for the initial segment j < J, Markov's inequality, and the continuity of measures along the union over J.
- paley_zygmund_half: if E X^2 = 1 and E X^4 <= K, then P(|X| >= 1/2) >= 9 / (16 K) (paley_zygmund of moments.v for X^2).
- dense_seq_rV: every nonempty set D of row vectors contains a sequence that is dense in D, from rational approximations (rat_approx_rV).
- small_ball_linear: let F : T -> 'rV[R]_N, S a square matrix, K > 0 and D a set of row vectors such that, for p in D and k < n, E_k <F, p>^2 = p S p^T > 0 and E_k <F, p>^4 <= K (p S p^T)^2, where <., .> is mxdot. If Psi is measurable in x, with
|(1/n) sum_k eps_k <F(x_k), p>| <= sqrt (p S p^T) Psi(x, eps)
for p in D, and E rademacher_mean (Psi x) <= r, then there is a measurable event of probability at most 512 K r / 9 outside of which
(1/n) sum_k <F(x_k), p>^2 >= 9 / (512 K) p S p^T
for every p in D. Proof: small_ball_method for the normalized class on a dense sequence of D, with u = 1/4 and q = 9 / (16 K) from paley_zygmund_half, and the continuity of quadratic forms (mxdot_form_lipschitz, mxdot_form_outer). Removing the ridge (Lemma 2.12) uses it with the features augmented by a constant coordinate for the bias.
- Moments of affine images, used for the affine forms of Lemma 2.12: integrable_pow4 (a finite fourth moment makes X and X^2 integrable), integral_affine_sqr, E (X - b)^2 = E X^2 - 2 b E X + b^2, integral_affine_pow4_le, E (X - b)^4 <= 8 (E X^4 + b^4), and markov_ge0, P(Y > B) <= E Y / B for Y >= 0 and B > 0.
ramp u x | min 1 (max 0 (|x| / u - 1)) |
small_ | the x : n.-tuple T for which some f_j has sum_k f_j(x_k)^2 < c |
Main results
| Results | Statement |
|---|---|
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. |
Declarations22 exported
Context {R : realType}.
forall {R : realType}, R -> R -> RDefinition ramp (u x : R) : R := Num.min 1 (Num.max 0 (`|x| / u - 1)).
The ramp from 0 on [-u, u] to 1 outside ]-2 u, 2 u[.
Used by 8 declarations in 1 file
- this file: ramp_ge0, ramp_le1, ramp0, ramp1, ramp_sqr, ramp_lipschitz, measurable_ramp, small_ball_method
forall {R : realType} (u x : R), 0 <= ramp u x
Statement as written in the source
Lemma ramp_ge0 u x : 0 <= ramp u x.
Used by 1 declaration in 1 file
- this file: small_ball_method
forall {R : realType} (u x : R), ramp u x <= 1
Statement as written in the source
Lemma ramp_le1 u x : ramp u x <= 1.
Used by 2 declarations in 1 file
- this file: ramp_sqr, small_ball_method
forall {R : realType} (u : R), ramp u 0 = 0
Statement as written in the source
Lemma ramp0 u : ramp u 0 = 0.
Used by 1 declaration in 1 file
- this file: small_ball_method
forall {R : realType} [u : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R] [x : R], 0 < u -> 2 * u <= `|x| -> ramp u x = 1
Statement as written in the source
Lemma ramp1 u x : 0 < u -> 2 * u <= `|x| -> ramp u x = 1.
Used by 1 declaration in 1 file
- this file: small_ball_method
forall {R : realType} [u : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R] (x : R), 0 < u -> u ^+ 2 * ramp u x <= x ^+ 2
Statement as written in the source
Lemma ramp_sqr u x : 0 < u -> u ^+ 2 * ramp u x <= x ^+ 2.
Used by 1 declaration in 1 file
- this file: small_ball_method
forall {R : realType} (a b : R), `|minr 1 (maxr 0 a) - minr 1 (maxr 0 b)| <= `|a - b|Statement as written in the source
Lemma clamp01_lipschitz (a b : R) : `|Num.min 1 (Num.max 0 a) - Num.min 1 (Num.max 0 b)| <= `|a - b|.
Used by 1 declaration in 1 file
- this file: ramp_lipschitz
forall {R : realType} [u : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R] (x y : R), 0 < u -> `|ramp u x - ramp u y| <= u^-1 * `|x - y|
Stated in the README together with small_ball_method.
Statement as written in the source
Used by 1 declaration in 1 file
- this file: small_ball_method
forall {R : realType} (u : R), measurable_fun [set: R] (ramp u)
Statement as written in the source
Lemma measurable_ramp u : measurable_fun [set: R] (ramp u).
Used by 1 declaration in 1 file
- this file: small_ball_method
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope.
forall {d : measure_display} {T : measurableType d} {R : realType} (n : nat), (nat -> T -> R) -> R -> set (n.-tuple T)
Definition small_ball_event n (f : nat -> T -> R) (c : R) := [set x : n.-tuple T | exists j, (\sum_(k < n) f j (tnth x k) ^+ 2 < c)%R].
The event that some f_j has an empirical second moment below c / n.
Used by 3 declarations in 1 file
Arguments small_ball_event : clear implicits.
forall [d : measure_display] [T : measurableType d] [R : realType] [n : nat] [f : nat -> T -> R] (c : R), (forall j : nat, measurable_fun [set: T] (f j)) -> (measure_tuple_display d).-measurable (small_ball_event n f c)
Stated in the README together with small_ball_method.
Statement as written in the source
Lemma measurable_small_ball_event n (f : nat -> T -> R) c : (forall j, measurable_fun [set: T] (f j)) -> measurable (small_ball_event n f c).
Used by 1 declaration in 1 file
- this file: small_ball_linear
forall [d : measure_display] [T : measurableType d] [R : realType] [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [u q r : R], (0 < n)%N -> 0 < u -> 0 < q -> (forall j : nat, measurable_fun [set: T] (f j)) -> (forall j k : nat, (k < n)%N -> (q%:E <= mu k [set t | (2 * u <= `|f j t|)%R])%E) -> (forall J : nat, (\int[tuple_prod mu n]_x (rademacher_mean (fun s : n.-tuple bool => max_norm (fun j : 'I_J => n%:R^-1 * \sum_(k < n) rademacher (tnth s k) * f j (tnth x k))))%:E <= r%:E)%E) -> (tuple_prod mu n (small_ball_event n f (n%:R * (u ^+ 2 * q / 2))) <= (8 * r / (u * q))%:E)%E
Mendelson's small-ball method in Markov form, for a sequence of functions.
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.
Statement as written in the source
Theorem small_ball_method (mu : nat -> probability T R) n (f : nat -> T -> R) (u q r : R) : (0 < n)%N -> (0 < u)%R -> (0 < q)%R -> (forall j, measurable_fun [set: T] (f j)) -> (forall j k, (k < n)%N -> q%:E <= mu k [set t | (2 * u <= `|f j t|)%R]) -> (forall J, \int[tuple_prod mu n]_x (rademacher_mean (fun s : n.-tuple bool => max_norm (fun j : 'I_J => n%:R^-1 * \sum_(k < n) rademacher (tnth s k) * f j (tnth x k))))%:E <= r%:E) -> tuple_prod mu n (small_ball_event n f (n%:R * (u ^+ 2 * q / 2))) <= (8 * r / (u * q))%:E.
Used by 1 declaration in 1 file
- this file: small_ball_linear
Arguments small_ball_event {d T R} n f c.
Context {R : realType}.
forall {R : realType} [N : nat] (x : 'rV_N) [e : R], 0 < e -> exists q : 'rV_N, frobenius (x - map_mx ratr q) < e
Statement as written in the source
Lemma rat_approx_rV N (x : 'rV[R]_N) (e : R) : 0 < e -> exists q : 'rV[rat]_N, frobenius (x - map_mx ratr q) < e.
Used by 1 declaration in 1 file
- this file: dense_seq_rV
forall {R : realType} [N : nat] [D : set 'rV_N], D !=set0 -> exists p : nat -> 'rV_N, (forall j : nat, D (p j)) /\ (forall x : 'rV_N, D x -> forall e : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R, 0 < e -> exists j : nat, frobenius (p j - x) < e)
Every nonempty set of row vectors has a dense sequence of its points.
Stated in the README together with small_ball_linear.
Statement as written in the source
Lemma dense_seq_rV N (D : set 'rV[R]_N) : D !=set0 -> exists p : nat -> 'rV[R]_N, (forall j, D (p j)) /\ forall x, D x -> forall e, 0 < e -> exists j, frobenius (p j - x) < e.
Used by 1 declaration in 1 file
- this file: small_ball_linear
forall {R : realType} [N : nat] (Q : 'M_N) (p p' : 'rV_N), `|mxdot (p *m Q) p - mxdot (p' *m Q) p'| <= frobenius Q * (frobenius p + frobenius p') * frobenius (p - p')
Quadratic forms are Lipschitz on bounded sets.
Statement as written in the source
Used by 1 declaration in 1 file
- this file: small_ball_linear
Statement as written in the source
Used by 1 declaration in 1 file
- this file: small_ball_linear
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R] [K : R], measurable_fun [set: T] X -> 0 < K -> (\int[P]_t (X t ^+ 2)%:E)%E = 1%E -> (\int[P]_t (X t ^+ 4)%:E <= K%:E)%E -> ((9 / (16 * K))%:E <= P [set t | (2^-1 <= `|X t|)%R])%E
A small-ball probability from the second and fourth moments.
Stated in the README together with small_ball_linear.
Statement as written in the source
Lemma paley_zygmund_half (P : probability T R) (X : T -> R) (K : R) : measurable_fun [set: T] X -> (0 < K)%R -> \int[P]_t (X t ^+ 2)%:E = 1 -> \int[P]_t (X t ^+ 4)%:E <= K%:E -> (9 / (16 * K))%:E <= P [set t | (2^-1 <= `|X t|)%R].
Used by 1 declaration in 1 file
- this file: small_ball_linear
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType] [mu : nat -> probability T R] [n N : nat] [F : T -> 'rV_N] [S0 : 'M_N] [D : set 'rV_N] [K r : R] [Psi : n.-tuple T -> n.-tuple bool -> R], (0 < n)%N -> 0 < K -> 0 <= r -> (forall p : 'rV_N, measurable_fun [set: T] (fun t : T => mxdot (F t) p)) -> (forall p : 'rV_N, D p -> 0 < mxdot (p *m S0) p) -> (forall (p : 'rV_N) (k : nat), D p -> (k < n)%N -> (\int[mu k]_t (mxdot (F t) p ^+ 2)%:E)%E = (mxdot (p *m S0) p)%:E) -> (forall (p : 'rV_N) (k : nat), D p -> (k < n)%N -> (\int[mu k]_t (mxdot (F t) p ^+ 4)%:E <= (K * mxdot (p *m S0) p ^+ 2)%:E)%E) -> (forall s : n.-tuple bool, measurable_fun [set: n.-tuple T] (Psi^~ s)) -> (forall (x : n.-tuple T) (s : n.-tuple bool) (p : 'rV_N), D p -> `|n%:R^-1 * \sum_(k < n) rademacher (tnth s k) * mxdot (F (tnth x k)) p| <= Num.ExtraDef.sqrtr (mxdot (p *m S0) p) * Psi x s) -> (\int[tuple_prod mu n]_x (rademacher_mean (Psi x))%:E <= r%:E)%E -> exists E : set (n.-tuple T), [/\ (measure_tuple_display d).-measurable E, (tuple_prod mu n E <= (512 * K * r / 9)%:E)%E & forall x : n.-tuple T, ~ E x -> forall p : 'rV_N, D p -> 9 / (512 * K) * mxdot (p *m S0) p <= n%:R^-1 * \sum_(k < n) mxdot (F (tnth x k)) p ^+ 2]
The small-ball method for a linear class with comparable second and fourth moments.
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.
Statement as written in the source
Theorem small_ball_linear (mu : nat -> probability T R) (n N : nat) (F : T -> 'rV[R]_N) (S : 'M[R]_N) (D : set 'rV[R]_N) (K r : R) (Psi : n.-tuple T -> n.-tuple bool -> R) : (0 < n)%N -> (0 < K)%R -> (0 <= r)%R -> (forall p, measurable_fun [set: T] (fun t => mxdot (F t) p)) -> (forall p, D p -> 0 < mxdot (p *m S) p)%R -> (forall p k, D p -> (k < n)%N -> \int[mu k]_t (mxdot (F t) p ^+ 2)%:E = (mxdot (p *m S) p)%:E) -> (forall p k, D p -> (k < n)%N -> \int[mu k]_t (mxdot (F t) p ^+ 4)%:E <= (K * mxdot (p *m S) p ^+ 2)%:E) -> (forall s, measurable_fun [set: n.-tuple T] (Psi ^~ s)) -> (forall x s p, D p -> `|n%:R^-1 * \sum_(k < n) rademacher (tnth s k) * mxdot (F (tnth x k)) p| <= Num.sqrt (mxdot (p *m S) p) * Psi x s)%R -> \int[tuple_prod mu n]_x (rademacher_mean (Psi x))%:E <= r%:E -> exists E : set (n.-tuple T), [/\ measurable E, tuple_prod mu n E <= (512 * K * r / 9)%:E & forall x, ~ E x -> forall p, D p -> (9 / (512 * K) * mxdot (p *m S) p <= n%:R^-1 * \sum_(k < n) mxdot (F (tnth x k)) p ^+ 2)%R].
Context d (T : measurableType d) (R : realType) (P : probability T R). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R], measurable_fun [set: T] X -> (\int[P]_t (X t ^+ 4)%:E < +oo)%E -> P.-integrable [set: T] (EFin \o X) /\ P.-integrable [set: T] (EFin \o (fun t : T => X t ^+ 2))
A finite fourth moment gives integrable first and second powers.
Statement as written in the source
Lemma integrable_pow4 (X : T -> R) : measurable_fun [set: T] X -> \int[P]_t (X t ^+ 4)%:E < +oo -> P.-integrable [set: T] (EFin \o X) /\ P.-integrable [set: T] (EFin \o (fun t => X t ^+ 2)%R).
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R] (b : R), P.-integrable [set: T] (EFin \o X) -> P.-integrable [set: T] (EFin \o (fun t : T => X t ^+ 2)) -> (\int[P]_t ((X t - b) ^+ 2)%:E)%E = (\int[P]_t (X t ^+ 2)%:E - (2 * b)%:E * \int[P]_t (X t)%:E + (b ^+ 2)%:E)%E
Statement as written in the source
Lemma integral_affine_sqr (X : T -> R) (b : R) : P.-integrable [set: T] (EFin \o X) -> P.-integrable [set: T] (EFin \o (fun t => X t ^+ 2)%R) -> \int[P]_t ((X t - b) ^+ 2)%:E = \int[P]_t (X t ^+ 2)%:E - (2 * b)%:E * \int[P]_t (X t)%:E + (b ^+ 2)%:E.
forall [d : measure_display] [T : measurableType d] [R : realType] (P : probability T R) [X : T -> R] (b : R), measurable_fun [set: T] X -> (\int[P]_t ((X t - b) ^+ 4)%:E <= 8 * (\int[P]_t (X t ^+ 4)%:E + (b ^+ 4)%:E))%E
Statement as written in the source
Lemma integral_affine_pow4_le (X : T -> R) (b : R) : measurable_fun [set: T] X -> \int[P]_t ((X t - b) ^+ 4)%:E <= 8%:E * (\int[P]_t (X t ^+ 4)%:E + (b ^+ 4)%:E).
forall [d : measure_display] [T : measurableType d] [R : realType] (P : probability T R) [Y : T -> R] [B : R], measurable_fun [set: T] Y -> (forall t : T, 0 <= Y t) -> 0 < B -> (P [set t | (B < Y t)%R] <= (B^-1)%:E * \int[P]_t (Y t)%:E)%E
Markov's inequality.
Statement as written in the source
Lemma markov_ge0 (Y : T -> R) (B : R) : measurable_fun [set: T] Y -> (forall t, 0 <= Y t)%R -> (0 < B)%R -> P [set t | (B < Y t)%R] <= (B^-1)%:E * \int[P]_t (Y t)%:E.