GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisfouriersmall_ball

The vector small-ball estimate

GaussianAnalysis.fourier.small_balllibrary/fourier/small_ball.v794 lines21 lemmas and theoremssource
Imports 13 library modules and 35 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.finite_group.fingroup, mathcomp.finite_group.perm, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, mathcomp.algebra.interval, mathcomp.algebra.archimedean, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.classical.cardinality, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.algebra.interval_inference, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.analysis.numfun, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.trigo, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.probability_theory.normal_distribution

Imported by 1
Required by 1 files of the paper proofs

For independent real x_1, ..., x_n of laws mu_1, ..., mu_n (tuple_prod) and row vectors w_1, ..., w_n of 'rV[R]_m with |w_k| <= rho and sum_k <x, w_k>^2 >= |x|^2 for all x, the probability that sum_k x_k w_k lies in a closed ball of radius eta sqrt m is at most (C eta)^m for eta >= C rho (vector_small_ball). The constant C depends only on v, lambda and eps when E[x_k^2] <= v and conc_fun mu_k lambda <= 1 - eps; in the form of Koehler and Sohn (arXiv 2608.27372, Proposition 2.4), for laws of mean zero and variance one with E[x^2 1_{|x| <= M}] >= 1/2, it depends only on M (vector_small_ball_moments). The level 1/2 may be any c > 0 (vector_small_ball_moments_level), and E[x_k^2] <= v may be replaced by E[(x_k - a_k)^2] <= v for any centers a_k, the means for instance (vector_small_ball_variance). The proof is Fourier-analytic, after Ball and Nazarov, and Rudelson and Vershynin:

  • Frames. If sum_k w_k^T w_k = I_m, then |theta|^2 = sum_k <theta, w_k>^2 (frame_mxdot) and sum_k |w_k|^2 = m (frame_trace). The regularized modulus exp (- s^2 |theta|^2 / 2) |cf nu theta| of the law nu of sum_k x_k w_k is then the product over k of |cf mu_k <w_k, theta>| exp (- s^2 <w_k, theta>^2 / 2) (cf_rV_norm_frame).
  • Lemma 3.8 of the paper (cf_rV_regularized_le). If, for each k with r = |w_k| > 0,
    \int |cf mu_k u|^(1 / r^2) exp (- s^2 u^2 / (2 r^2)) du <= r C,

    then \int exp (- s^2 |theta|^2 / 2) |cf nu theta| dtheta <= C^m. This is the Brascamp-Lieb inequality with u_k = w_k / |w_k| and c_k = |w_k|^2 (brascamp_lieb_ge0 allows zero weights), after the change of variables u = |w_k| t.

  • Removing the Gaussian. For G of law gauss m independent of Y and 2 m s^2 <= d^2, P(|Y - z| <= r) <= 2 P(|Y + s G - z| <= r + d) (ball_le_add_gauss), and the latter is bounded by the regularized integral and the volume of the ball (add_gauss_ball_le). If the regularized integral is at most C^m and 2 s^2 <= eta^2, then P(|Y - z| <= eta sqrt m) <= (sqrt (8 e / pi) C eta)^m (small_ball_of_cf_bound).
  • Whitening. A matrix W with W (sum_k w_k^T w_k) W^T = I_m and |x W| <= |x| turns the w_k into a frame w_k W^T (frame_mulmx) and does not shrink the balls (tuple_prod_ball_mulmx, contraction_trmx).

vector_small_ball_fourier puts these together, with the constant max (2, sqrt (8 e / pi) C), for laws that satisfy the bound above for all 0 < r <= s <= 1/2 (Lemma 3.5 of the paper).

Sources. The Brascamp-Lieb inequality is brascamp_lieb of comparison/brascamp_lieb_lebesgue.v, which derives it from the Gaussian form for bounded functions, gauss_brascamp_lieb_bounded of comparison/brascamp_lieb.v. The bound of Lemma 3.5 and its first half are gauss_factor_exists and conc_fun_truncated_exists of fourier/gauss_factor.v, and the whitening matrix is whitening_exists of matrix/whitening.v.

Main results

ResultsStatement
lee_prodpowR_sum
Products of nonnegative extended reals are monotone, and x^(\sum_i c_i) = \prod_i x^(c_i) for x > 0.
frame_mxdotframe_tracemulmx_outer_rV
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.
cf_rV_norm_frame
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).
ball_le_add_gaussadd_gauss_ball_lesmall_ball_of_cf_bound
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.
contraction_trmxtuple_prod_ball_mulmxframe_mulmxmeasurable_tuple_sum_rVmeasurable_tuple_ball_rV
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.
brascamp_lieb_ge0
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/brascamp_lieb_lebesgue.v) by reindexing.
cf_rV_regularized_le
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.
vector_small_ball_fourier
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).
vector_small_ball
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.
vector_small_ball_moments
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.
vector_small_ball_moments_level
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.
vector_small_ball_variance
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.

Declarations21 exported, 2 local

lemma, theoremdefinitioninstancelocal
sectionprod_power
Context {R : realType}.
lemma lee_prod main result source, line 88 
forall {R : realType} [I : Type] (r : seq I) [P : pred I] [f g : I -> \bar R],
(forall i : I, P i -> (0%R <= f i)%E) ->
(forall i : I, P i -> (f i <= g i)%E) ->
(\prod_(i <- r | P i) f i <= \prod_(i <- r | P i) g i)%E

Products of nonnegative extended reals are monotone.

Main result, as the README states it

Products of nonnegative extended reals are monotone, and x^(\sum_i c_i) = \prod_i x^(c_i) for x > 0.

Statement as written in the source
Lemma lee_prod I (r : seq I) (P : pred I) (f g : I -> \bar R) :
  (forall i, P i -> 0 <= f i)%E -> (forall i, P i -> f i <= g i)%E ->
  (\prod_(i <- r | P i) f i <= \prod_(i <- r | P i) g i)%E.
Used by 1 declaration in 1 file
lemma powR_sum main result source, line 98 
forall {R : realType} [x : R] [I : Type] (r : seq I) (P : pred I) (c : I -> R),
0 < x -> x `^ (\sum_(i <- r | P i) c i) = \prod_(i <- r | P i) x `^ c i

x^(sum_i c_i) = prod_i x^(c_i) for x > 0.

Main result

Stated in the README together with lee_prod.

Statement as written in the source
Lemma powR_sum (x : R) I (r : seq I) (P : pred I) (c : I -> R) : 0 < x ->
  x `^ (\sum_(i <- r | P i) c i) = \prod_(i <- r | P i) x `^ c i.
Used by 1 declaration in 1 file
sectionframe
Context {R : realType} {m : nat}.
lemma mulmx_outer_rV main result source, line 113 
forall {R : realType} {m : nat} (theta w : 'rV_m), theta *m (w^T *m w) = mxdot theta w *: w

theta (w^T w) = <theta, w> w.

Main result

Stated in the README together with frame_mxdot.

Statement as written in the source
Lemma mulmx_outer_rV (theta w : 'rV[R]_m) :
  theta *m (w^T *m w) = mxdot theta w *: w.
Used by 3 declarations in 1 file
lemma frame_mxdot main result source, line 121 
forall {R : realType} {m : nat} [I : Type] [r : seq I] [P : pred I] 
  [w : I -> 'rV_m] (theta : 'rV_m),
\sum_(k <- r | P k) (w k)^T *m w k = 1%:M ->
mxdot theta theta = \sum_(k <- r | P k) mxdot theta (w k) ^+ 2

A frame (sum_k w_k^T w_k = I_m) preserves the norm: |theta|^2 = sum_k <theta, w_k>^2.

Main result, as the README states it

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.

Statement as written in the source
Lemma frame_mxdot I (r : seq I) (P : pred I) (w : I -> 'rV[R]_m)
    (theta : 'rV[R]_m) :
  \sum_(k <- r | P k) (w k)^T *m w k = 1%:M ->
  mxdot theta theta = \sum_(k <- r | P k) mxdot theta (w k) ^+ 2.
Used by 1 declaration in 1 file
lemma frame_trace main result source, line 133 
forall {R : realType} {m : nat} [I : Type] [r : seq I] [P : pred I] [w : I -> 'rV_m],
\sum_(k <- r | P k) (w k)^T *m w k = 1%:M -> \sum_(k <- r | P k) mxdot (w k) (w k) = m%:R

The trace of a frame: sum_k |w_k|^2 = m.

Main result

Stated in the README together with frame_mxdot.

Statement as written in the source
Lemma frame_trace I (r : seq I) (P : pred I) (w : I -> 'rV[R]_m) :
  \sum_(k <- r | P k) (w k)^T *m w k = 1%:M ->
  \sum_(k <- r | P k) mxdot (w k) (w k) = m%:R.
Used by 1 declaration in 1 file
sectionframe_cf
Context {R : realType} {m : nat}.
lemma cf_rV_norm_frame main result source, line 150 
forall {R : realType} {m : nat} [mu : nat -> probability (measurableTypeR R) R] 
  [n : nat] [w : nat -> 'rV_m] [nu : probability 'rV_m R] (s : R),
(forall A : set 'rV_m,
 (measure_matrix_display default_measure_display).-measurable A ->
 tuple_prod mu n ((fun x : n.-tuple R => \sum_(k < n) tnth x k *: w k) @^-1` A) = nu A) ->
\sum_(k < n) (w k)^T *m w k = 1%:M ->
forall theta : 'rV_m,
expR (- s ^+ 2 * mxdot theta theta / 2) * cf_rV_norm nu theta =
\prod_(k < n)
   (cf_norm (mu k) (mxdot (w k) theta) * expR (- s ^+ 2 * mxdot (w k) theta ^+ 2 / 2))

For x of law tuple_prod mu n and a frame w, the regularized modulus exp (- s^2 |theta|^2 / 2) |cf nu theta| of the law nu of sum_k x_k w_k is a product of one-dimensional factors.

Main result, as the README states it

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).

Statement as written in the source
Lemma cf_rV_norm_frame (mu : nat -> probability (measurableTypeR R) R) n
    (w : nat -> 'rV[R]_m) (nu : probability 'rV[R]_m R) (s : R) :
  (forall A : set 'rV[R]_m, measurable A ->
     tuple_prod mu n ((fun x => \sum_(k < n) tnth x k *: w k) @^-1` A) =
     nu A) ->
  \sum_(k < n) (w k)^T *m w k = 1%:M ->
  forall theta,
    expR (- s ^+ 2 * mxdot theta theta / 2) * cf_rV_norm nu theta =
    \prod_(k < n) (cf_norm (mu k) (mxdot (w k) theta) *
                   expR (- s ^+ 2 * mxdot (w k) theta ^+ 2 / 2)).
Used by 1 declaration in 1 file
sectionremove_gauss
Context {R : realType} {m : nat}.
Local Open Scope ereal_scope.
lemma ball_le_add_gauss main result source, line 174 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) [s r d : R] (z : 'rV_m),
0 < s ->
0 <= r ->
0 < d ->
2 * m%:R * s ^+ 2 <= d ^+ 2 ->
(nu [set y | (frobenius (y - z) <= r)%R] <=
 2 * (nu \x gauss m) [set p | (frobenius (p.1 + s *: p.2 - z) <= r + d)%R])%E

Removing the Gaussian: if 2 m s^2 <= d^2, P(|Y - z| <= r) is at most twice P(|Y + s G - z| <= r + d), for G of law gauss m independent of Y.

Main result, as the README states it

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.

Statement as written in the source
Lemma ball_le_add_gauss (nu : probability 'rV[R]_m R) (s r d : R)
    (z : 'rV[R]_m) :
  (0 < s)%R -> (0 <= r)%R -> (0 < d)%R ->
  (2 * m%:R * s ^+ 2 <= d ^+ 2)%R ->
  nu [set y | (frobenius (y - z) <= r)%R] <=
  2%:E * (nu \x gauss m) [set p | (frobenius (p.1 + s *: p.2 - z) <= r + d)%R].
Used by 1 declaration in 1 file
lemma add_gauss_ball_le main result source, line 234 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) [s r : R] (z : 'rV_m),
0 < s ->
0 < r ->
((nu \x gauss m) [set p | (frobenius (p.1 + s *: p.2 - z) <= r)%R] <=
 ((2 * pi) ^- m)%:E *
 \int[lebesgue_rV m]_th (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E *
 ((Num.ExtraDef.sqrtr (2 * pi * expR 1 / m%:R) * r) ^+ m)%:E)%E

The regularized law on a ball: P(|Y + s G - z| <= r) is at most (2 pi)^-m (\int |cf nu| exp (- s^2 |theta|^2 / 2)) (sqrt (2 pi e / m) r)^m.

Main result

Stated in the README together with ball_le_add_gauss.

Statement as written in the source
Lemma add_gauss_ball_le (nu : probability 'rV[R]_m R) (s r : R)
    (z : 'rV[R]_m) : (0 < s)%R -> (0 < r)%R ->
  (nu \x gauss m) [set p | (frobenius (p.1 + s *: p.2 - z) <= r)%R] <=
  ((2 * pi) ^- m)%:E *
  \int[lebesgue_rV m]_th
    (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E *
  ((Num.sqrt (2 * pi * expR 1 / m%:R) * r) ^+ m)%:E.
Used by 1 declaration in 1 file
let sqrt_const section-local source, line 251 
Let sqrt_const (eta : R) : (0 < m)%N -> (0 <= eta)%R ->
  (Num.sqrt (2 * pi * expR 1 / m%:R) *
    (eta * Num.sqrt m%:R + eta * Num.sqrt m%:R) / (2 * pi) =
   Num.sqrt (2 * expR 1 / pi) * eta)%R.
Used by 1 declaration in 1 file
lemma small_ball_of_cf_bound main result source, line 284 
forall {R : realType} {m : nat} [nu : probability 'rV_m R] [s C eta : R] (z : 'rV_m),
(0 < m)%N ->
0 < s ->
0 < eta ->
2 * s ^+ 2 <= eta ^+ 2 ->
0 <= C ->
(\int[lebesgue_rV m]_th (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E <=
 (C ^+ m)%:E)%E ->
(nu [set y | (frobenius (y - z) <= eta * Num.ExtraDef.sqrtr m%:R)%R] <=
 ((Num.ExtraDef.sqrtr (8 * expR 1 / pi) * C * eta) ^+ m)%:E)%E

If the regularized integral is at most C^m and 2 s^2 <= eta^2, then P(|Y - z| <= eta sqrt m) <= (sqrt (8 e / pi) C eta)^m.

Main result

Stated in the README together with ball_le_add_gauss.

Statement as written in the source
Lemma small_ball_of_cf_bound (nu : probability 'rV[R]_m R) (s C eta : R)
    (z : 'rV[R]_m) :
  (0 < m)%N -> (0 < s)%R -> (0 < eta)%R -> (2 * s ^+ 2 <= eta ^+ 2)%R ->
  (0 <= C)%R ->
  \int[lebesgue_rV m]_th
    (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E <= (C ^+ m)%:E ->
  nu [set y | (frobenius (y - z) <= eta * Num.sqrt m%:R)%R] <=
  ((Num.sqrt (8 * expR 1 / pi) * C * eta) ^+ m)%:E.
Used by 1 declaration in 1 file
sectionwhitening_reduction
Context {R : realType} {m : nat}.
lemma contraction_trmx main result source, line 336 
forall {R : realType} {m : nat} [W : 'M_m],
(forall x : 'rV_m, frobenius (x *m W) <= frobenius x) ->
forall y : 'rV_m, frobenius (y *m W^T) <= frobenius y

If x |-> x W does not increase the Euclidean norm, neither does y |-> y W^T.

Main result, as the README states it

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.

Statement as written in the source
Lemma contraction_trmx (W : 'M[R]_m) :
  (forall x : 'rV[R]_m, frobenius (x *m W) <= frobenius x) ->
  forall y : 'rV[R]_m, frobenius (y *m W^T) <= frobenius y.
Used by 1 declaration in 1 file
lemma measurable_tuple_sum_rV main result source, line 353 
forall {R : realType} {m : nat} [n : nat] (w : nat -> 'rV_m),
measurable_fun [set: n.-tuple (measurableTypeR R)]
  (fun x : n.-tuple _ =>
   \sum_(k < n) tnth x k *: w k)

The map x |-> sum_k x_k w_k on n-tuples, and the events |sum_k x_k w_k - z| <= t, are measurable.

Main result

Stated in the README together with contraction_trmx.

Statement as written in the source
Lemma measurable_tuple_sum_rV n (w : nat -> 'rV[R]_m) :
  measurable_fun [set: n.-tuple (measurableTypeR R)]
    (fun x => \sum_(k < n) tnth x k *: w k).
Used by 2 declarations in 1 file
lemma measurable_tuple_ball_rV main result source, line 364 
forall {R : realType} {m : nat} [n : nat] (w : nat -> 'rV_m) (z : 'rV_m) (t : R),
(measure_tuple_display ((R.-ocitv).-measurable).-sigma).-measurable
  [set x | frobenius (\sum_(k < n) tnth x k *: w k - z) <= t]
Main result

Stated in the README together with contraction_trmx.

Statement as written in the source
Lemma measurable_tuple_ball_rV n (w : nat -> 'rV[R]_m) (z : 'rV[R]_m)
    (t : R) :
  measurable [set x : n.-tuple (measurableTypeR R) |
    frobenius (\sum_(k < n) tnth x k *: w k - z) <= t].
Used by 3 declarations in 2 files
lemma tuple_prod_ball_mulmx main result source, line 376 
forall {R : realType} {m : nat} (mu : nat -> probability (measurableTypeR R) R) 
  (n : nat) (w : nat -> 'rV_m) [A : 'M_m] (z : 'rV_m) (t : R),
(forall y : 'rV_m, frobenius (y *m A) <= frobenius y) ->
(tuple_prod mu n [set x | (frobenius (\sum_(k < n) tnth x k *: w k - z) <= t)%R] <=
 tuple_prod mu n
   [set x | (frobenius (\sum_(k < n) tnth x k *: (w k *m A) - z *m A) <= t)%R])%E

Whitening: if y |-> y A does not increase the norm, the event |sum_k x_k w_k - z| <= t is contained in |sum_k x_k (w_k A) - z A| <= t.

Main result

Stated in the README together with contraction_trmx.

Statement as written in the source
Lemma tuple_prod_ball_mulmx (mu : nat -> probability (measurableTypeR R) R)
    n (w : nat -> 'rV[R]_m) (A : 'M[R]_m) (z : 'rV[R]_m) (t : R) :
  (forall y : 'rV[R]_m, frobenius (y *m A) <= frobenius y) ->
  (tuple_prod mu n
     [set x | (frobenius (\sum_(k < n) tnth x k *: w k - z) <= t)%R] <=
   tuple_prod mu n
     [set x |
       (frobenius (\sum_(k < n) tnth x k *: (w k *m A) - z *m A) <= t)%R])%E.
Used by 1 declaration in 1 file
lemma frame_mulmx main result source, line 397 
forall {R : realType} {m : nat} [n : nat] [w : nat -> 'rV_m] [W : 'M_m],
W *m (\sum_(k < n) (w k)^T *m w k) *m W^T = 1%:M ->
\sum_(k < n) (w k *m W^T)^T *m (w k *m W^T) = 1%:M

If W S W^T = I_m for S = sum_k w_k^T w_k, the w_k W^T form a frame.

Main result

Stated in the README together with contraction_trmx.

Statement as written in the source
Lemma frame_mulmx n (w : nat -> 'rV[R]_m) (W : 'M[R]_m) :
  W *m (\sum_(k < n) (w k)^T *m w k) *m W^T = 1%:M ->
  \sum_(k < n) (w k *m W^T)^T *m (w k *m W^T) = 1%:M.
Used by 1 declaration in 1 file
sectionsmall_ball
Context {R : realType}.
lemma brascamp_lieb_ge0 main result source, line 412 
forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R]
  [F : 'I_n -> R -> \bar R],
(forall i : 'I_n, 0 < c i -> mxdot (u i) (u i) = 1) ->
(forall i : 'I_n, 0 <= c i) ->
\sum_i c i *: ((u i)^T *m u i) = 1%:M ->
(forall i : 'I_n, measurable_fun [set: R] (F i)) ->
(forall (i : 'I_n) (t : R), (0%R <= F i t)%E) ->
(\int[lebesgue_rV m]_x \prod_i F i (mxdot x (u i)) `^ c i <=
 \prod_i (\int[lebesgue_measure]_t F i t) `^ c i)%E

The Brascamp-Lieb inequality with nonnegative weights: the unit vectors are only required where the weight is positive.

Main result, as the README states it

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/brascamp_lieb_lebesgue.v) by reindexing.

Statement as written in the source
Lemma brascamp_lieb_ge0 m n (u : 'I_n -> 'rV[R]_m) (c : 'I_n -> R)
    (F : 'I_n -> R -> \bar R) :
  (forall i, 0 < c i -> mxdot (u i) (u i) = 1) -> (forall i, 0 <= c i) ->
  \sum_i c i *: ((u i)^T *m u i) = 1%:M ->
  (forall i, measurable_fun [set: R] (F i)) -> (forall i t, 0 <= F i t)%E ->
  (\int[lebesgue_rV m]_x \prod_i F i (mxdot x (u i)) `^ c i <=
   \prod_i (\int[lebesgue_measure]_t F i t) `^ c i)%E.
Used by 1 declaration in 1 file
lemma cf_rV_regularized_le main result source, line 452 
forall {R : realType} [m : nat] [mu : nat -> probability (measurableTypeR R) R] 
  [n : nat] [w : nat -> 'rV_m] [nu : probability 'rV_m R] [s C : R],
(forall A : set 'rV_m,
 (measure_matrix_display default_measure_display).-measurable A ->
 tuple_prod mu n ((fun x : n.-tuple R => \sum_(k < n) tnth x k *: w k) @^-1` A) = nu A) ->
\sum_(k < n) (w k)^T *m w k = 1%:M ->
0 < C ->
(forall k : nat,
 (k < n)%N ->
 w k != 0 ->
 (\int[lebesgue_measure]_u
     (cf_norm (mu k) u `^ (frobenius (w k) ^- 2) *
      expR (- s ^+ 2 * u ^+ 2 / (2 * frobenius (w k) ^+ 2)))%:E <=
  (frobenius (w k) * C)%:E)%E) ->
(\int[lebesgue_rV m]_th (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E <=
 (C ^+ m)%:E)%E

Lemma 3.8 of Koehler and Sohn: for the law nu of sum_k x_k w_k, x of law tuple_prod mu n and w a frame, if the one-dimensional factor of each nonzero w_k is at most r C, r = |w_k|, then the regularized integral of |cf nu| is at most C^m.

Main result, as the README states it

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.

Statement as written in the source
Lemma cf_rV_regularized_le m (mu : nat -> probability (measurableTypeR R) R) n
    (w : nat -> 'rV[R]_m) (nu : probability 'rV[R]_m R) (s C : R) :
  (forall A : set 'rV[R]_m, measurable A ->
     tuple_prod mu n ((fun x => \sum_(k < n) tnth x k *: w k) @^-1` A) =
     nu A) ->
  \sum_(k < n) (w k)^T *m w k = 1%:M -> 0 < C ->
  (forall k, (k < n)%N -> w k != 0 ->
     (\int[lebesgue_measure]_u
        (cf_norm (mu k) u `^ (frobenius (w k) ^- 2) *
         expR (- s ^+ 2 * u ^+ 2 / (2 * frobenius (w k) ^+ 2)))%:E <=
      (frobenius (w k) * C)%:E)%E) ->
  (\int[lebesgue_rV m]_th
     (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E <=
   (C ^+ m)%:E)%E.
Used by 1 declaration in 1 file
let vector_small_ball_of section-local source, line 570 
Let vector_small_ball_of m (mu : nat -> probability (measurableTypeR R) R)
    n (w : nat -> 'rV[R]_m) (W : 'M[R]_m) (z : 'rV[R]_m) (rho eta C : R) :
  (0 < m)%N ->
  W *m (\sum_(k < n) (w k)^T *m w k) *m W^T = 1%:M ->
  (forall x : 'rV[R]_m, frobenius (x *m W) <= frobenius x) ->
  0 < rho -> (forall k, (k < n)%N -> frobenius (w k) <= rho) -> 0 < C ->
  (forall k r, (k < n)%N -> 0 < r <= rho ->
     (\int[lebesgue_measure]_u
        (cf_norm (mu k) u `^ (r ^- 2) *
         expR (- rho ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <= (r * C)%:E)%E) ->
  0 < eta -> 2 * rho ^+ 2 <= eta ^+ 2 ->
  (tuple_prod mu n [set x | (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
     eta * Num.sqrt m%:R)%R] <=
   ((Num.sqrt (8 * expR 1 / pi) * C * eta) ^+ m)%:E)%E.

The vector small-ball estimate, given a whitening matrix W and the bound r C on the one-dimensional factors of Lemma 3.8 at s = rho.

Used by 1 declaration in 1 file
theorem vector_small_ball_fourier main result source, line 614 
forall {R : realType} [m : nat] [mu : nat -> probability (measurableTypeR R) R] 
  [n : nat] [w : nat -> 'rV_m] [W : 'M_m] (z : 'rV_m) [rho eta C : R],
W *m (\sum_(k < n) (w k)^T *m w k) *m W^T = 1%:M ->
(forall x : 'rV_m, frobenius (x *m W) <= frobenius x) ->
0 < rho ->
(forall k : nat, (k < n)%N -> frobenius (w k) <= rho) ->
0 < C ->
(forall (k : nat)
   (r s : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R),
 (k < n)%N ->
 0 < r <= s ->
 s <= 2^-1 ->
 (\int[lebesgue_measure]_u
     (cf_norm (mu k) u `^ (r ^- 2) * expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <=
  (r * C)%:E)%E) ->
maxr 2 (Num.ExtraDef.sqrtr (8 * expR 1 / pi) * C) * rho <= eta ->
(tuple_prod mu n
   [set x | (frobenius (\sum_(k < n) tnth x k *: w k - z) <= eta * Num.ExtraDef.sqrtr m%:R)%R] <=
 ((maxr 2 (Num.ExtraDef.sqrtr (8 * expR 1 / pi) * C) * eta) ^+ m)%:E)%E

The vector small-ball estimate with an explicit constant, for laws whose characteristic functions satisfy the one-dimensional bound of Lemma 3.5 with constant C, given a whitening matrix W of the frame.

Main result, as the README states it

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).

Statement as written in the source
Theorem vector_small_ball_fourier m
    (mu : nat -> probability (measurableTypeR R) R) n (w : nat -> 'rV[R]_m)
    (W : 'M[R]_m) (z : 'rV[R]_m) (rho eta C : R) :
  W *m (\sum_(k < n) (w k)^T *m w k) *m W^T = 1%:M ->
  (forall x : 'rV[R]_m, frobenius (x *m W) <= frobenius x) ->
  0 < rho -> (forall k, (k < n)%N -> frobenius (w k) <= rho) -> 0 < C ->
  (forall k r s, (k < n)%N -> 0 < r <= s -> s <= 2^-1 ->
     (\int[lebesgue_measure]_u
        (cf_norm (mu k) u `^ (r ^- 2) *
         expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <= (r * C)%:E)%E) ->
  maxr 2 (Num.sqrt (8 * expR 1 / pi) * C) * rho <= eta ->
  (tuple_prod mu n [set x | (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
     eta * Num.sqrt m%:R)%R] <=
   ((maxr 2 (Num.sqrt (8 * expR 1 / pi) * C) * eta) ^+ m)%:E)%E.
Used by 2 declarations in 1 file
theorem vector_small_ball main result source, line 658 
forall {R : realType} [v lambda eps : R],
0 < v ->
0 < lambda ->
0 < eps ->
exists2 C : R,
  0 < C &
  forall (m n : nat) (mu : nat -> probability (measurableTypeR R) R) 
    (w : nat -> 'rV_m) (z : 'rV_m) (rho eta : R),
  (forall k : nat, (k < n)%N -> (\int[mu k]_x (x ^+ 2)%:E <= v%:E)%E) ->
  (forall k : nat, (k < n)%N -> conc_fun (mu k) lambda <= 1 - eps) ->
  (forall x : 'rV_m, mxdot x x <= \sum_(k < n) mxdot x (w k) ^+ 2) ->
  0 < rho ->
  (forall k : nat, (k < n)%N -> frobenius (w k) <= rho) ->
  C * rho <= eta ->
  (tuple_prod mu n
     [set x | (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
               eta * Num.ExtraDef.sqrtr m%:R)%R] <=
   ((C * eta) ^+ m)%:E)%E

The vector small-ball estimate.

Main result, as the README states it

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.

Statement as written in the source
Theorem vector_small_ball (v lambda eps : R) :
  0 < v -> 0 < lambda -> 0 < eps ->
  exists2 C : R, 0 < C &
  forall m n (mu : nat -> probability (measurableTypeR R) R)
      (w : nat -> 'rV[R]_m) (z : 'rV[R]_m) (rho eta : R),
    (forall k, (k < n)%N -> (\int[mu k]_x ((x ^+ 2)%R)%:E <= v%:E)%E) ->
    (forall k, (k < n)%N -> conc_fun (mu k) lambda <= 1 - eps) ->
    (forall x : 'rV[R]_m, mxdot x x <= \sum_(k < n) mxdot x (w k) ^+ 2) ->
    0 < rho -> (forall k, (k < n)%N -> frobenius (w k) <= rho) ->
    C * rho <= eta ->
    (tuple_prod mu n [set x |
       (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
        eta * Num.sqrt m%:R)%R] <= ((C * eta) ^+ m)%:E)%E.
Used by 2 declarations in 1 file
theorem vector_small_ball_moments main result source, line 696 
forall {R : realType} [M : R],
0 < M ->
exists2 C : R,
  0 < C &
  forall (m n : nat) (mu : nat -> probability (measurableTypeR R) R) 
    (w : nat -> 'rV_m) (z : 'rV_m) (rho eta : R),
  (forall k : nat, (k < n)%N -> (\int[mu k]_x x%:E)%E = 0) ->
  (forall k : nat, (k < n)%N -> (\int[mu k]_x (x ^+ 2)%:E)%E = 1%E) ->
  (forall k : nat,
   (k < n)%N -> ((2^-1)%:E <= \int[mu k]_x (x ^+ 2 * \1_[set y | `|y| <= M] x)%:E)%E) ->
  (forall x : 'rV_m, mxdot x x <= \sum_(k < n) mxdot x (w k) ^+ 2) ->
  0 < rho ->
  (forall k : nat, (k < n)%N -> frobenius (w k) <= rho) ->
  C * rho <= eta ->
  (tuple_prod mu n
     [set x | (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
               eta * Num.ExtraDef.sqrtr m%:R)%R] <=
   ((C * eta) ^+ m)%:E)%E

The vector small-ball estimate in the form of Proposition 2.4 of Koehler and Sohn: laws of mean zero and variance one with E[x^2 1_{|x| <= M}] >= 1/2.

Main result, as the README states it

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.

Statement as written in the source
Theorem vector_small_ball_moments (M : R) : 0 < M ->
  exists2 C : R, 0 < C &
  forall m n (mu : nat -> probability (measurableTypeR R) R)
      (w : nat -> 'rV[R]_m) (z : 'rV[R]_m) (rho eta : R),
    (forall k, (k < n)%N -> (\int[mu k]_x x%:E = 0)%E) ->
    (forall k, (k < n)%N -> (\int[mu k]_x ((x ^+ 2)%R)%:E = 1)%E) ->
    (forall k, (k < n)%N -> ((2^-1)%:E <=
       \int[mu k]_x ((x ^+ 2 * \1_[set y | `|y| <= M] x)%R)%:E)%E) ->
    (forall x : 'rV[R]_m, mxdot x x <= \sum_(k < n) mxdot x (w k) ^+ 2) ->
    0 < rho -> (forall k, (k < n)%N -> frobenius (w k) <= rho) ->
    C * rho <= eta ->
    (tuple_prod mu n [set x |
       (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
        eta * Num.sqrt m%:R)%R] <= ((C * eta) ^+ m)%:E)%E.
theorem vector_small_ball_moments_level main result source, line 726 
forall {R : realType} [M c : R],
0 < M ->
0 < c ->
exists2 C : R,
  0 < C &
  forall (m n : nat) (mu : nat -> probability (measurableTypeR R) R) 
    (w : nat -> 'rV_m) (z : 'rV_m) (rho eta : R),
  (forall k : nat, (k < n)%N -> (\int[mu k]_x x%:E)%E = 0) ->
  (forall k : nat, (k < n)%N -> (\int[mu k]_x (x ^+ 2)%:E)%E = 1%E) ->
  (forall k : nat,
   (k < n)%N -> (c%:E <= \int[mu k]_x (x ^+ 2 * \1_[set y | `|y| <= M] x)%:E)%E) ->
  (forall x : 'rV_m, mxdot x x <= \sum_(k < n) mxdot x (w k) ^+ 2) ->
  0 < rho ->
  (forall k : nat, (k < n)%N -> frobenius (w k) <= rho) ->
  C * rho <= eta ->
  (tuple_prod mu n
     [set x | (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
               eta * Num.ExtraDef.sqrtr m%:R)%R] <=
   ((C * eta) ^+ m)%:E)%E

The vector small-ball estimate for laws of mean zero and variance one with E[x^2 1_{|x| <= M}] >= c, for any level c > 0.

Main result, as the README states it

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.

Statement as written in the source
Theorem vector_small_ball_moments_level (M c : R) : 0 < M -> 0 < c ->
  exists2 C : R, 0 < C &
  forall m n (mu : nat -> probability (measurableTypeR R) R)
      (w : nat -> 'rV[R]_m) (z : 'rV[R]_m) (rho eta : R),
    (forall k, (k < n)%N -> (\int[mu k]_x x%:E = 0)%E) ->
    (forall k, (k < n)%N -> (\int[mu k]_x ((x ^+ 2)%R)%:E = 1)%E) ->
    (forall k, (k < n)%N -> (c%:E <=
       \int[mu k]_x ((x ^+ 2 * \1_[set y | `|y| <= M] x)%R)%:E)%E) ->
    (forall x : 'rV[R]_m, mxdot x x <= \sum_(k < n) mxdot x (w k) ^+ 2) ->
    0 < rho -> (forall k, (k < n)%N -> frobenius (w k) <= rho) ->
    C * rho <= eta ->
    (tuple_prod mu n [set x |
       (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
        eta * Num.sqrt m%:R)%R] <= ((C * eta) ^+ m)%:E)%E.
theorem vector_small_ball_variance main result source, line 758 
forall {R : realType} [v lambda eps : R],
0 < v ->
0 < lambda ->
0 < eps ->
exists2 C : R,
  0 < C &
  forall (m n : nat) (mu : nat -> probability (measurableTypeR R) R) 
    (a : nat -> R) (w : nat -> 'rV_m) (z : 'rV_m) (rho eta : R),
  (forall k : nat, (k < n)%N -> (\int[mu k]_x ((x - a k) ^+ 2)%:E <= v%:E)%E) ->
  (forall k : nat, (k < n)%N -> conc_fun (mu k) lambda <= 1 - eps) ->
  (forall x : 'rV_m, mxdot x x <= \sum_(k < n) mxdot x (w k) ^+ 2) ->
  0 < rho ->
  (forall k : nat, (k < n)%N -> frobenius (w k) <= rho) ->
  C * rho <= eta ->
  (tuple_prod mu n
     [set x | (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
               eta * Num.ExtraDef.sqrtr m%:R)%R] <=
   ((C * eta) ^+ m)%:E)%E

The vector small-ball estimate under E[(x - a_k)^2] <= v, for instance the variance when a_k is the mean of mu k.

Main result, as the README states it

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.

Statement as written in the source
Theorem vector_small_ball_variance (v lambda eps : R) :
  0 < v -> 0 < lambda -> 0 < eps ->
  exists2 C : R, 0 < C &
  forall m n (mu : nat -> probability (measurableTypeR R) R) (a : nat -> R)
      (w : nat -> 'rV[R]_m) (z : 'rV[R]_m) (rho eta : R),
    (forall k, (k < n)%N ->
       (\int[mu k]_x (((x - a k) ^+ 2)%R)%:E <= v%:E)%E) ->
    (forall k, (k < n)%N -> conc_fun (mu k) lambda <= 1 - eps) ->
    (forall x : 'rV[R]_m, mxdot x x <= \sum_(k < n) mxdot x (w k) ^+ 2) ->
    0 < rho -> (forall k, (k < n)%N -> frobenius (w k) <= rho) ->
    C * rho <= eta ->
    (tuple_prod mu n [set x |
       (frobenius (\sum_(k < n) tnth x k *: w k - z) <=
        eta * Num.sqrt m%:R)%R] <= ((C * eta) ^+ m)%:E)%E.
Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.