GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysiscomparisonescape

Escape through a mesh and norms of Gaussian matrices

GaussianAnalysis.comparison.escapelibrary/comparison/escape.v1,430 lines72 lemmas and theorems, 10 definitionssource
Imports 15 library modules and 28 external

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.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_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.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.numfun, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.probability_theory.normal_distribution

Imported by 7
Required by 9 files of the paper proofs

Let a have law gauss (N * M), so that G = vec_mx a is an N x M matrix of independent standard normal entries, and let g and h have laws gauss N and gauss M. Vectors x of R^M are column vectors 'cV[R]_M, and |x| is frobenius x.

For a nonempty set T of unit vectors of 'cV[R]_M and N > 0, gordon_escape is Gordon's escape theorem: 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. By Gaussian concentration, inf_(x in T) |G x| is at most E[|g|] - w(T) - u with probability at most expR (- u^2 / 2) (gordon_escape_tail). So when w(T) < E[|g|], the kernel of G misses T with high probability: escape through a mesh. For T the unit sphere, w(T) = E[|h|] (gwidth_sphere), which bounds the smallest singular value of G (gauss_min_singular_mean).

For a second nonempty set Y of unit vectors of 'cV[R]_N, gordon_minmax is Gordon's comparison for the min-max of the bilinear form: E[inf_(x in T) sup_(y in Y) <y, G x>] >= w(Y) - w(T), with w(Y) = E[sup_(y in Y) <g, y>]. Let Y be the unit vectors of the range of an orthogonal projection P != 0 of 'cV[R]_N. Then sup_(y in Y) <y, v> is |P v| (gwidth_range_sphere), so E[inf_(x in T) |P G x|] >= E[|g P|] - w(T) (gordon_projection), with the Gaussian tail of gordon_escape_tail (gordon_projection_tail). Since E[|g A|^2] = |A|^2 (gauss_sqr_mulmx), the Gaussian Poincare inequality gives E[|g P|] >= sqrt (tr P - 1) (gauss_proj_mean_ge). So for M > 0, inf_(|x| = 1) |P G x| is at most sqrt (tr P - 1) - sqrt M - u with probability at most expR (- u^2 / 2) (gauss_proj_singular_tail): the smallest singular value of G seen through P, for instance on the symmetric matrices.

For N, M > 0, E[opnorm G] <= E[|g|] + E[|h|] <= sqrt N + sqrt M (gauss_opnorm_mean, gauss_frobenius_mean_le, gauss_opnorm_mean_sqrt), and opnorm G exceeds E[|g|] + E[|h|] + u with probability at most expR (- u^2 / 2) (gauss_opnorm_tail).

The proofs compare, for finite families xs of unit vectors of 'cV[R]_M and ys of unit vectors of 'cV[R]_N, the matrix process ys t^T *m G *m xs u with the process <g, ys t> + <h, xs u>: by Gordon's inequality for the min-max over u and t (aux_bil_minmax), and by the Sudakov-Fernique inequality for the maximum (bil_aux_max). Nets of T and of the unit spheres (net_exists, unit_sphere_net) pass from finite families to T and to the spheres. The file also proves that gauss n is invariant under x |-> - x (integral_gauss_opp).

unvec kthe pair (i, j) such that mxvec_index i j = k
fam_mx xsthe matrix whose columns are the vectors xs u
bil_mx xs ysthe matrix B such that vec_mx (a *m B) u t is ys t ^T *m vec_mx a *m xs u
aux_mx xs ysthe matrix C such that vec_mx (z *m C) u t is <lsubmx z, ys t> + <rsubmx z, xs u>
gwidth_fun T hsup_(x in T) <h, x>, for h : 'rV[R]_M
escape_inf T Ginf_(x in T) |G *m x|
minmax_sph T Y Ginf_(x in T) sup_(y in Y) <y, G *m x>
range_sphere Pthe unit vectors y of 'cV[R]_N with P *m y = y

Main results

ResultsStatementUsed by theories/
gordon_escapegordon_escape_tail
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/EscapeExpectation
gauss_opnorm_meangauss_opnorm_mean_sqrtgauss_opnorm_tail
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).
gauss_min_singular_meangwidth_sphere
E[inf_(|x| = 1) |G x|] >= E[|g|] - E[|h|]: the Gaussian width of the unit sphere is E[|h|].
gauss_frobenius_mean_leintegral_gauss_opp
E[|g|] <= sqrt n for g of law gauss n, and gauss n is invariant under x |-> - x.Gaussian/Symmetric/Reflection
gordon_minmaxgordon_projectiongordon_projection_tailgauss_proj_mean_gegauss_proj_singular_tail
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).
aux_bil_minmaxbil_aux_maxauxT_bilT_minmax
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/Processes

Declarations82 exported, 9 local

lemma, theoremdefinitioninstancelocal
sectionunvec
Context {m n : nat}.
definition unvec source, line 90
Type
forall {m n : nat}, 'I_(m * n) -> 'I_m * 'I_n
Definition
Definition unvec (k : 'I_(m * n)) : 'I_m * 'I_n :=
  enum_val (cast_ord (esym (mxvec_cast m n)) k).

The inverse of mxvec_index.

Used by 8 declarations in 2 files
lemma unvecK source, line 93 
forall {m n : nat} (i : 'I_m) (j : 'I_n), unvec (mxvec_index i j) = (i, j)
Statement as written in the source
Lemma unvecK i j : unvec (mxvec_index i j) = (i, j).
Used by 14 declarations in 2 files
sectionrmax_minmax_sums
Context {R : realType}.
lemma rmax_addr source, line 101 
forall {R : realType} [q : nat] (z : 'rV_q.+1) (c : R),
rmax (\row_j (z 0 j + c)) = rmax z + c
Statement as written in the source
Lemma rmax_addr q (z : 'rV[R]_q.+1) c : rmax (\row_j (z 0 j + c)) = rmax z + c.
Used by 1 declaration in 1 file
lemma minmax_add source, line 109 
forall {R : realType} [p q : nat] (a : 'rV_q.+1) (c : 'rV_p.+1),
minmax (\matrix_(u, t) (c 0 u + a 0 t)) = rmax a - rmax (- c)

min_u max_t (c u + a t) = max_t a t + min_u c u.

Statement as written in the source
Lemma minmax_add p q (a : 'rV[R]_q.+1) (c : 'rV[R]_p.+1) :
  minmax (\matrix_(u, t) (c 0 u + a 0 t)) = rmax a - rmax (- c).
Used by 1 declaration in 1 file
lemma rmax_vec_add source, line 123 
forall {R : realType} [p q : nat] [w : 'rV_(p.+1 * q.+1)] [a : 'rV_q.+1] [c : 'rV_p.+1],
(forall (u : 'I_p.+1) (t : 'I_q.+1), w 0 (mxvec_index u t) = c 0 u + a 0 t) ->
rmax w = rmax c + rmax a

The largest coordinate of the vector of the c u + a t over all pairs.

Statement as written in the source
Lemma rmax_vec_add p q (w : 'rV[R]_(p.+1 * q.+1)) (a : 'rV[R]_q.+1)
    (c : 'rV[R]_p.+1) :
  (forall u t, w 0 (mxvec_index u t) = c 0 u + a 0 t) ->
  rmax w = rmax c + rmax a.
Used by 1 declaration in 1 file
sectiongauss_opp
Context {R : realType} {n : nat}.
lemma ge0_integral_gauss_opp source, line 141 
forall {R : realType} {n : nat} [f : 'rV_n -> \bar R],
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, (0%R <= f x)%E) ->
(\int[gauss n]_x f (- x)%R)%E = (\int[gauss n]_x f x)%E
Statement as written in the source
Lemma ge0_integral_gauss_opp (f : 'rV[R]_n -> \bar R) :
  measurable_fun setT f -> (forall x, 0 <= f x)%E ->
  (\int[gauss n]_x f (- x)%R = \int[gauss n]_x f x)%E.
Used by 3 declarations in 2 files
lemma integrable_gauss_opp source, line 155 
forall {R : realType} {n : nat} [f : 'rV_n -> \bar R],
(gauss n).-integrable [set: 'rV_n] f ->
(gauss n).-integrable [set: 'rV_n] (fun x : 'rV_n => f (- x))
Statement as written in the source
Lemma integrable_gauss_opp (f : 'rV[R]_n -> \bar R) :
  (gauss n).-integrable setT f -> (gauss n).-integrable setT (fun x => f (- x)%R).
Used by 1 declaration in 1 file
lemma integral_gauss_opp main result source, line 167 
forall {R : realType} {n : nat} [f : 'rV_n -> \bar R],
(gauss n).-integrable [set: 'rV_n] f ->
(\int[gauss n]_x f (- x)%R)%E = (\int[gauss n]_x f x)%E
Main result

Stated in the README together with gauss_frobenius_mean_le.

Statement as written in the source
Lemma integral_gauss_opp (f : 'rV[R]_n -> \bar R) :
  (gauss n).-integrable setT f ->
  (\int[gauss n]_x f (- x)%R = \int[gauss n]_x f x)%E.
Used by 3 declarations in 3 files
sectionfrobenius_vec_mx
Context {R : realType}.
lemma frobenius_vec_mx source, line 184 
forall {R : realType} [m n : nat] (z : 'rV_(m * n)), frobenius (vec_mx z) = frobenius z
Statement as written in the source
Lemma frobenius_vec_mx m n (z : 'rV[R]_(m * n)) :
  frobenius (vec_mx z) = frobenius z.
Used by 18 declarations in 4 files
sectionfam_mx
Context {R : realType} {n k : nat}.
definition fam_mx source, line 197
Type
forall {R : realType} {n k : nat}, ('I_k -> 'cV_n) -> 'M_(n, k)
Definition
Definition fam_mx (xs : 'I_k -> 'cV[R]_n) : 'M[R]_(n, k) := \matrix_(j, u) xs u j 0.

The matrix whose columns are the xs u.

Used by 13 declarations in 2 files
lemma fam_mxE source, line 199 
forall {R : realType} {n k : nat} (xs : 'I_k -> 'cV_n) (h : 'rV_n) (u : 'I_k),
(h *m fam_mx xs) 0 u = mxdot h^T (xs u)
Statement as written in the source
Lemma fam_mxE (xs : 'I_k -> 'cV[R]_n) (h : 'rV[R]_n) u :
  (h *m fam_mx xs) 0 u = mxdot h^T (xs u).
Used by 7 declarations in 2 files
sectionbilinear_process
Context {R : realType} {N M k l : nat}.
Variables (xs : 'I_k.+1 -> 'cV[R]_M) (ys : 'I_l.+1 -> 'cV[R]_N).
Local Notation idx := (@mxvec_index k.+1 l.+1).
definition bil_mx source, line 212
Type
forall {R : realType} {N M k l : nat},
('I_k.+1 -> 'cV_M) -> ('I_l.+1 -> 'cV_N) -> 'M_(N * M, k.+1 * l.+1)
Definition
Definition bil_mx : 'M[R]_(N * M, k.+1 * l.+1) :=
  \matrix_(r, c) (ys (unvec c).2 (unvec r).1 0 * xs (unvec c).1 (unvec r).2 0).

For a of law gauss (N * M), the Gaussian matrix with rows indexed by xs and columns by ys whose entry (u, t) is ys t ^T *m vec_mx a *m xs u.

Used by 11 declarations in 2 files
definition aux_mx source, line 217
Type
forall {R : realType} {N M k l : nat},
('I_k.+1 -> 'cV_M) -> ('I_l.+1 -> 'cV_N) -> 'M_(N + M, k.+1 * l.+1)
Definition
Definition aux_mx : 'M[R]_(N + M, k.+1 * l.+1) :=
  col_mx (\matrix_(i, c) ys (unvec c).2 i 0) (\matrix_(j, c) xs (unvec c).1 j 0).

For z of law gauss (N + M), the Gaussian matrix whose entry (u, t) is <lsubmx z, ys t> + <rsubmx z, xs u>.

Used by 12 declarations in 1 file
lemma bil_mxE source, line 220 
forall {R : realType} {N M k l : nat} (xs : 'I_k.+1 -> 'cV_M) (ys : 'I_l.+1 -> 'cV_N)
  (a : 'rV_(N * M)) (u : 'I_k.+1) (t : 'I_l.+1),
vec_mx (a *m bil_mx xs ys) u t = mxdot (ys t) (vec_mx a *m xs u)
Statement as written in the source
Lemma bil_mxE (a : 'rV[R]_(N * M)) u t :
  vec_mx (a *m bil_mx) u t = mxdot (ys t) (vec_mx a *m xs u).
Used by 4 declarations in 2 files
lemma aux_mxE source, line 228 
forall {R : realType} {N M k l : nat} (xs : 'I_k.+1 -> 'cV_M) (ys : 'I_l.+1 -> 'cV_N)
  (z : 'rV_(N + M)) (u : 'I_k.+1) (t : 'I_l.+1),
vec_mx (z *m aux_mx xs ys) u t = mxdot (lsubmx z)^T (ys t) + mxdot (rsubmx z)^T (xs u)
Statement as written in the source
Lemma aux_mxE (z : 'rV[R]_(N + M)) u t :
  vec_mx (z *m aux_mx) u t =
  mxdot (lsubmx z)^T (ys t) + mxdot (rsubmx z)^T (xs u).
Used by 2 declarations in 1 file
lemma bil_cov source, line 236 
forall {R : realType} {N M k l : nat} (xs : 'I_k.+1 -> 'cV_M) (ys : 'I_l.+1 -> 'cV_N)
  (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
((bil_mx xs ys)^T *m bil_mx xs ys) (mxvec_index u t) (mxvec_index v s) =
mxdot (ys t) (ys s) * mxdot (xs u) (xs v)
Statement as written in the source
Lemma bil_cov u t v s :
  (bil_mx^T *m bil_mx) (idx u t) (idx v s) =
  mxdot (ys t) (ys s) * mxdot (xs u) (xs v).
Used by 2 declarations in 2 files
lemma aux_cov source, line 245 
forall {R : realType} {N M k l : nat} (xs : 'I_k.+1 -> 'cV_M) (ys : 'I_l.+1 -> 'cV_N)
  (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
((aux_mx xs ys)^T *m aux_mx xs ys) (mxvec_index u t) (mxvec_index v s) =
mxdot (ys t) (ys s) + mxdot (xs u) (xs v)
Statement as written in the source
Lemma aux_cov u t v s :
  (aux_mx^T *m aux_mx) (idx u t) (idx v s) =
  mxdot (ys t) (ys s) + mxdot (xs u) (xs v).
Used by 1 declaration in 1 file
lemma minmax_aux source, line 253 
forall {R : realType} {N M k l : nat} (xs : 'I_k.+1 -> 'cV_M) (ys : 'I_l.+1 -> 'cV_N)
  (z : 'rV_(N + M)),
minmax (vec_mx (z *m aux_mx xs ys)) =
rmax (lsubmx z *m fam_mx ys) - rmax (- rsubmx z *m fam_mx xs)
Statement as written in the source
Lemma minmax_aux (z : 'rV[R]_(N + M)) :
  minmax (vec_mx (z *m aux_mx)) =
  rmax (lsubmx z *m fam_mx ys) - rmax ((- rsubmx z) *m fam_mx xs).
Used by 1 declaration in 1 file
lemma rmax_aux source, line 263 
forall {R : realType} {N M k l : nat} (xs : 'I_k.+1 -> 'cV_M) (ys : 'I_l.+1 -> 'cV_N)
  (z : 'rV_(N + M)),
rmax (z *m aux_mx xs ys) = rmax (rsubmx z *m fam_mx xs) + rmax (lsubmx z *m fam_mx ys)
Statement as written in the source
Lemma rmax_aux (z : 'rV[R]_(N + M)) :
  rmax (z *m aux_mx) =
  rmax (rsubmx z *m fam_mx xs) + rmax (lsubmx z *m fam_mx ys).
Used by 1 declaration in 1 file
let lsub_fam section-local source, line 272 
Let lsub_fam (z : 'rV[R]_(N + M)) :
  lsubmx z *m fam_mx ys = z *m col_mx (fam_mx ys) 0.
Used by 2 declarations in 1 file
let rsub_fam section-local source, line 276 
Let rsub_fam (z : 'rV[R]_(N + M)) :
  (- rsubmx z) *m fam_mx xs = z *m col_mx 0 (- fam_mx xs).
Used by 1 declaration in 1 file
lemma integral_minmax_aux source, line 282 
forall {R : realType} {N M k l : nat} (xs : 'I_k.+1 -> 'cV_M) (ys : 'I_l.+1 -> 'cV_N),
\int[gauss (N + M)]_z minmax (vec_mx (z *m aux_mx xs ys)) =
\int[gauss N]_g rmax (g *m fam_mx ys) - \int[gauss M]_h rmax (h *m fam_mx xs)
Statement as written in the source
Lemma integral_minmax_aux :
  \int[gauss (N + M)]_z minmax (vec_mx (z *m aux_mx)) =
  \int[gauss N]_g rmax (g *m fam_mx ys) - \int[gauss M]_h rmax (h *m fam_mx xs).
Used by 2 declarations in 1 file
let rsub_fam' section-local source, line 301 
Let rsub_fam' (z : 'rV[R]_(N + M)) :
  rsubmx z *m fam_mx xs = z *m col_mx 0 (fam_mx xs).
Used by 1 declaration in 1 file
lemma integral_rmax_aux source, line 305 
forall {R : realType} {N M k l : nat} (xs : 'I_k.+1 -> 'cV_M) (ys : 'I_l.+1 -> 'cV_N),
\int[gauss (N + M)]_z rmax (z *m aux_mx xs ys) =
\int[gauss M]_h rmax (h *m fam_mx xs) + \int[gauss N]_g rmax (g *m fam_mx ys)
Statement as written in the source
Lemma integral_rmax_aux :
  \int[gauss (N + M)]_z rmax (z *m aux_mx) =
  \int[gauss M]_h rmax (h *m fam_mx xs) + \int[gauss N]_g rmax (g *m fam_mx ys).
Used by 1 declaration in 1 file
Hypothesis xs1 : forall u, frobenius (xs u) = 1.
Hypothesis ys1 : forall t, frobenius (ys t) = 1.
let dot1 section-local source, line 326 
Let dot1 n (x y : 'cV[R]_n) : frobenius x = 1 -> frobenius y = 1 ->
  mxdot x y <= 1.
Used by 2 declarations in 1 file
let sq1 section-local source, line 330 
Let sq1 n (x : 'cV[R]_n) : frobenius x = 1 -> mxdot x x = 1.
Used by 2 declarations in 1 file
lemma incr_var_bil_aux source, line 333 
forall {R : realType} {N M k l : nat} [xs : 'I_k.+1 -> 'cV_M] [ys : 'I_l.+1 -> 'cV_N],
(forall u : 'I_k.+1, frobenius (xs u) = 1) ->
(forall t : 'I_l.+1, frobenius (ys t) = 1) ->
forall (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
incr_var (aux_mx xs ys) (mxvec_index u t) (mxvec_index v s) -
incr_var (bil_mx xs ys) (mxvec_index u t) (mxvec_index v s) =
2 * (1 - mxdot (ys t) (ys s)) * (1 - mxdot (xs u) (xs v))
Statement as written in the source
Lemma incr_var_bil_aux u t v s :
  incr_var aux_mx (idx u t) (idx v s) - incr_var bil_mx (idx u t) (idx v s) =
  2 * (1 - mxdot (ys t) (ys s)) * (1 - mxdot (xs u) (xs v)).
Used by 2 declarations in 1 file
lemma bil_aux_max main result source, line 339 
forall {R : realType} {N M k l : nat} [xs : 'I_k.+1 -> 'cV_M] [ys : 'I_l.+1 -> 'cV_N],
(forall u : 'I_k.+1, frobenius (xs u) = 1) ->
(forall t : 'I_l.+1, frobenius (ys t) = 1) ->
(\int[gauss (N * M)]_a (rmax (a *m bil_mx xs ys))%:E <=
 \int[gauss (N + M)]_z (rmax (z *m aux_mx xs ys))%:E)%E

The Sudakov-Fernique comparison of the two processes.

Main result

Stated in the README together with aux_bil_minmax.

Statement as written in the source
Lemma bil_aux_max :
  (\int[gauss (N * M)]_a (rmax (a *m bil_mx))%:E <=
   \int[gauss (N + M)]_z (rmax (z *m aux_mx))%:E)%E.
Used by 1 declaration in 1 file
lemma aux_bil_minmax main result source, line 351 
forall {R : realType} {N M k l : nat} [xs : 'I_k.+1 -> 'cV_M] [ys : 'I_l.+1 -> 'cV_N],
(forall u : 'I_k.+1, frobenius (xs u) = 1) ->
(forall t : 'I_l.+1, frobenius (ys t) = 1) ->
(\int[gauss (N + M)]_z (minmax (vec_mx (z *m aux_mx xs ys)))%:E <=
 \int[gauss (N * M)]_a (minmax (vec_mx (a *m bil_mx xs ys)))%:E)%E

Gordon's comparison of the two processes.

Main result, as the README states it

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

Used in theories/ by: Gordon/Processes
Statement as written in the source
Lemma aux_bil_minmax :
  (\int[gauss (N + M)]_z (minmax (vec_mx (z *m aux_mx)))%:E <=
   \int[gauss (N * M)]_a (minmax (vec_mx (a *m bil_mx)))%:E)%E.
Used by 2 declarations in 1 file
sectionbilinear_processT
Context {R : realType} {N M k l : nat}.
Variables (zs : 'I_k.+1 -> 'cV[R]_N) (vs : 'I_l.+1 -> 'cV[R]_M).
Local Notation idx := (@mxvec_index k.+1 l.+1).
definition bilT_mx source, line 370
Type
forall {R : realType} {N M k l : nat},
('I_k.+1 -> 'cV_N) -> ('I_l.+1 -> 'cV_M) -> 'M_(N * M, k.+1 * l.+1)
Definition
Definition bilT_mx : 'M[R]_(N * M, k.+1 * l.+1) :=
  \matrix_(r, c) (zs (unvec c).1 (unvec r).1 0 * vs (unvec c).2 (unvec r).2 0).

The process (u, t) |-> zs u ^T *m vec_mx a *m vs t, with the minimum over the left factor, and its auxiliary process.

Used by 5 declarations in 2 files
definition auxT_mx source, line 373
Type
forall {R : realType} {N M k l : nat},
('I_k.+1 -> 'cV_N) -> ('I_l.+1 -> 'cV_M) -> 'M_(N + M, k.+1 * l.+1)
Definition
Definition auxT_mx : 'M[R]_(N + M, k.+1 * l.+1) :=
  col_mx (\matrix_(i, c) zs (unvec c).1 i 0) (\matrix_(j, c) vs (unvec c).2 j 0).
Used by 4 declarations in 1 file
lemma bilT_mxE source, line 376 
forall {R : realType} {N M k l : nat} (zs : 'I_k.+1 -> 'cV_N) (vs : 'I_l.+1 -> 'cV_M)
  (a : 'rV_(N * M)) (u : 'I_k.+1) (t : 'I_l.+1),
vec_mx (a *m bilT_mx zs vs) u t = mxdot (zs u) (vec_mx a *m vs t)
Statement as written in the source
Lemma bilT_mxE (a : 'rV[R]_(N * M)) u t :
  vec_mx (a *m bilT_mx) u t = mxdot (zs u) (vec_mx a *m vs t).
Used by 1 declaration in 1 file
  • GaussianAnalysis.comparison.cgmt: XY_up
lemma auxT_mxE source, line 384 
forall {R : realType} {N M k l : nat} (zs : 'I_k.+1 -> 'cV_N) (vs : 'I_l.+1 -> 'cV_M)
  (z : 'rV_(N + M)) (u : 'I_k.+1) (t : 'I_l.+1),
vec_mx (z *m auxT_mx zs vs) u t = mxdot (lsubmx z)^T (zs u) + mxdot (rsubmx z)^T (vs t)
Statement as written in the source
Lemma auxT_mxE (z : 'rV[R]_(N + M)) u t :
  vec_mx (z *m auxT_mx) u t =
  mxdot (lsubmx z)^T (zs u) + mxdot (rsubmx z)^T (vs t).
lemma bilT_cov source, line 392 
forall {R : realType} {N M k l : nat} (zs : 'I_k.+1 -> 'cV_N) (vs : 'I_l.+1 -> 'cV_M)
  (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
((bilT_mx zs vs)^T *m bilT_mx zs vs) (mxvec_index u t) (mxvec_index v s) =
mxdot (zs u) (zs v) * mxdot (vs t) (vs s)
Statement as written in the source
Lemma bilT_cov u t v s :
  (bilT_mx^T *m bilT_mx) (idx u t) (idx v s) =
  mxdot (zs u) (zs v) * mxdot (vs t) (vs s).
Used by 2 declarations in 2 files
lemma auxT_cov source, line 401 
forall {R : realType} {N M k l : nat} (zs : 'I_k.+1 -> 'cV_N) (vs : 'I_l.+1 -> 'cV_M)
  (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
((auxT_mx zs vs)^T *m auxT_mx zs vs) (mxvec_index u t) (mxvec_index v s) =
mxdot (zs u) (zs v) + mxdot (vs t) (vs s)
Statement as written in the source
Lemma auxT_cov u t v s :
  (auxT_mx^T *m auxT_mx) (idx u t) (idx v s) =
  mxdot (zs u) (zs v) + mxdot (vs t) (vs s).
Used by 1 declaration in 1 file
Hypothesis zs1 : forall u, frobenius (zs u) = 1.
Hypothesis vs1 : forall t, frobenius (vs t) = 1.
let dot1 section-local source, line 412 
Let dot1 n (x y : 'cV[R]_n) : frobenius x = 1 -> frobenius y = 1 ->
  mxdot x y <= 1.
Used by 1 declaration in 1 file
let sq1 section-local source, line 416 
Let sq1 n (x : 'cV[R]_n) : frobenius x = 1 -> mxdot x x = 1.
Used by 2 declarations in 1 file
lemma incr_var_bilT_auxT source, line 419 
forall {R : realType} {N M k l : nat} [zs : 'I_k.+1 -> 'cV_N] [vs : 'I_l.+1 -> 'cV_M],
(forall u : 'I_k.+1, frobenius (zs u) = 1) ->
(forall t : 'I_l.+1, frobenius (vs t) = 1) ->
forall (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
incr_var (auxT_mx zs vs) (mxvec_index u t) (mxvec_index v s) -
incr_var (bilT_mx zs vs) (mxvec_index u t) (mxvec_index v s) =
2 * (1 - mxdot (zs u) (zs v)) * (1 - mxdot (vs t) (vs s))
Statement as written in the source
Lemma incr_var_bilT_auxT u t v s :
  incr_var auxT_mx (idx u t) (idx v s) - incr_var bilT_mx (idx u t) (idx v s) =
  2 * (1 - mxdot (zs u) (zs v)) * (1 - mxdot (vs t) (vs s)).
Used by 1 declaration in 1 file
lemma auxT_bilT_minmax main result source, line 425 
forall {R : realType} {N M k l : nat} [zs : 'I_k.+1 -> 'cV_N] [vs : 'I_l.+1 -> 'cV_M],
(forall u : 'I_k.+1, frobenius (zs u) = 1) ->
(forall t : 'I_l.+1, frobenius (vs t) = 1) ->
(\int[gauss (N + M)]_z (minmax (vec_mx (z *m auxT_mx zs vs)))%:E <=
 \int[gauss (N * M)]_a (minmax (vec_mx (a *m bilT_mx zs vs)))%:E)%E

Gordon's comparison of the two processes, with the minimum over u.

Main result

Stated in the README together with aux_bil_minmax.

Statement as written in the source
Lemma auxT_bilT_minmax :
  (\int[gauss (N + M)]_z (minmax (vec_mx (z *m auxT_mx)))%:E <=
   \int[gauss (N * M)]_a (minmax (vec_mx (a *m bilT_mx)))%:E)%E.
sectionwidth_escape
Context {R : realType} {M : nat}.
Variable T : set 'cV[R]_M.
Hypothesis T1 : forall x, T x -> frobenius x = 1.
Hypothesis T0 : T !=set0.
definition gwidth_fun source, line 445
Type
forall {R : realType} {M : nat}, set 'cV_M -> 'rV_M -> R
Definition
Definition gwidth_fun (h : 'rV[R]_M) : R := sup [set mxdot h^T x | x in T].

sup_(x in T) <h, x>, whose mean for h of law gauss M is the Gaussian width of T.

Used by 21 declarations in 1 file
let dot_le section-local source, line 447 
Let dot_le (h : 'rV[R]_M) x : T x -> mxdot h^T x <= frobenius h.
Used by 3 declarations in 1 file
lemma gwidth_ge source, line 452 
forall {R : realType} {M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
forall (h : 'rV_M) [x : 'cV_M], T x -> mxdot h^T x <= gwidth_fun T h
Statement as written in the source
Lemma gwidth_ge h x : T x -> mxdot h^T x <= gwidth_fun h.
Used by 6 declarations in 1 file
lemma gwidth_le source, line 458 
forall {R : realType} {M : nat} [T : set 'cV_M],
T !=set0 ->
forall [h : 'rV_M] [c : join_Num_NumDomain_between_GRing_ComNzRing_and_Order_Preorder R],
(forall x : 'cV_M, T x -> mxdot h^T x <= c) -> gwidth_fun T h <= c
Statement as written in the source
Lemma gwidth_le h c : (forall x, T x -> mxdot h^T x <= c) -> gwidth_fun h <= c.
Used by 5 declarations in 1 file
lemma gwidth_lipschitz source, line 464 
forall {R : realType} {M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
forall h h' : 'rV_M, `|gwidth_fun T h - gwidth_fun T h'| <= 1 * frobenius (h - h')
Statement as written in the source
Lemma gwidth_lipschitz h h' :
  `|gwidth_fun h - gwidth_fun h'| <= 1 * frobenius (h - h').
Used by 3 declarations in 1 file
lemma gwidth_norm source, line 477 
forall {R : realType} {M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 -> forall h : 'rV_M, `|gwidth_fun T h| <= frobenius h
Statement as written in the source
Lemma gwidth_norm h : `|gwidth_fun h| <= frobenius h.
Used by 1 declaration in 1 file
definition escape_inf source, line 486
Type
forall {R : realType} {M : nat}, set 'cV_M -> forall [N : nat], 'M_(N, M) -> R
Definition
Definition escape_inf N (G : 'M[R]_(N, M)) : R :=
  inf [set frobenius (G *m x) | x in T].

inf_(x in T) |G x|.

Used by 30 declarations in 3 files
lemma escape_inf_le source, line 489 
forall {R : realType} {M : nat} [T : set 'cV_M] [N : nat] (G : 'M_(N, M)) [x : 'cV_M],
T x -> escape_inf T G <= frobenius (G *m x)
Statement as written in the source
Lemma escape_inf_le N (G : 'M[R]_(N, M)) x :
  T x -> escape_inf G <= frobenius (G *m x).
Used by 4 declarations in 2 files
lemma escape_inf_ge source, line 496 
forall {R : realType} {M : nat} [T : set 'cV_M],
T !=set0 ->
forall [N : nat] [G : 'M_(N, M)] [c : R],
(forall x : 'cV_M, T x -> c <= frobenius (G *m x)) -> c <= escape_inf T G
Statement as written in the source
Lemma escape_inf_ge N (G : 'M[R]_(N, M)) c :
  (forall x, T x -> c <= frobenius (G *m x)) -> c <= escape_inf G.
Used by 5 declarations in 2 files
lemma escape_inf_lipschitz source, line 504 
forall {R : realType} {M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
forall [N : nat] (G G' : 'M_(N, M)),
`|escape_inf T G - escape_inf T G'| <= 1 * frobenius (G - G')
Statement as written in the source
Lemma escape_inf_lipschitz N (G G' : 'M[R]_(N, M)) :
  `|escape_inf G - escape_inf G'| <= 1 * frobenius (G - G').
Used by 3 declarations in 1 file
lemma escape_inf_ge0 source, line 518 
forall {R : realType} {M : nat} [T : set 'cV_M],
T !=set0 -> forall [N : nat] (G : 'M_(N, M)), 0 <= escape_inf T G
Statement as written in the source
Lemma escape_inf_ge0 N (G : 'M[R]_(N, M)) : 0 <= escape_inf G.
Used by 1 declaration in 1 file
lemma escape_inf_norm source, line 521 
forall {R : realType} {M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 -> forall [N : nat] (G : 'M_(N, M)), `|escape_inf T G| <= frobenius G
Statement as written in the source
Lemma escape_inf_norm N (G : 'M[R]_(N, M)) : `|escape_inf G| <= frobenius G.
sectionnet_max
Context {R : realType} {N : nat}.
lemma rmax_net_ge source, line 535 
forall {R : realType} {N : nat} [l : nat] [ys : 'I_l.+1 -> 'cV_N] [eta : R] (v : 'cV_N),
(forall y : 'cV_N, frobenius y = 1 -> exists t : 'I_l.+1, frobenius (y - ys t) <= eta) ->
(1 - eta) * frobenius v <= rmax (\row_t mxdot v (ys t))

If the family ys meets every ball of radius eta centered on the unit sphere, the largest of the <v, ys t> is at least (1 - eta) |v|.

Statement as written in the source
Lemma rmax_net_ge l (ys : 'I_l.+1 -> 'cV[R]_N) (eta : R) (v : 'cV[R]_N) :
  (forall y, frobenius y = 1 -> exists t, frobenius (y - ys t) <= eta) ->
  (1 - eta) * frobenius v <= rmax (\row_t mxdot v (ys t)).
Used by 1 declaration in 1 file
lemma net_family source, line 558 
forall {R : realType} {N : nat} [Ns : seq 'cV_N] [y0 : 'cV_N] [eta : R],
is_net (unit_sphere (n:=N)) (y0 :: Ns) eta ->
forall [y : 'cV_N],
frobenius y = 1 -> exists t : 'I_(size Ns).+1, frobenius (y - (y0 :: Ns)`_t) <= eta

An eta-net of the unit sphere, as a family indexed by an ordinal.

Statement as written in the source
Lemma net_family (Ns : seq 'cV[R]_N) (y0 : 'cV[R]_N) (eta : R) :
  is_net (@unit_sphere R N) (y0 :: Ns) eta ->
  forall y, frobenius y = 1 ->
    exists t : 'I_(size Ns).+1, frobenius (y - nth 0 (y0 :: Ns) t) <= eta.
Used by 1 declaration in 1 file
sectiongordon_escape
Context {R : realType} {N M : nat}.
Variable T : set 'cV[R]_M.
Hypothesis T1 : forall x, T x -> frobenius x = 1.
Hypothesis T0 : T !=set0.
lemma integrable_gwidth source, line 576 
forall {R : realType} {M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 -> (gauss M).-integrable [set: 'rV_M] (EFin \o gwidth_fun T)
Statement as written in the source
Lemma integrable_gwidth :
  (gauss M).-integrable [set: 'rV[R]_M] (EFin \o gwidth_fun T).
Used by 2 declarations in 1 file
lemma integrable_escape_inf source, line 582 
forall {R : realType} {N M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
(gauss (N * M)).-integrable [set: 'rV_(N * M)]
  (EFin \o (fun a : 'rV_(N * M) => escape_inf T (vec_mx a : 'M_(N, M))))
Statement as written in the source
Lemma integrable_escape_inf :
  (gauss (N * M)).-integrable [set: 'rV[R]_(N * M)]
    (EFin \o (fun a => escape_inf T (vec_mx a : 'M[R]_(N, M)))).
Used by 1 declaration in 1 file
lemma minmax_bil_le source, line 590 
forall {R : realType} {N M : nat} [T : set 'cV_M],
T !=set0 ->
forall [k l : nat] [xs : 'I_k.+1 -> 'cV_M] [ys : 'I_l.+1 -> 'cV_N] 
  [delta : R] (a : 'rV_(N * M)),
(forall t : 'I_l.+1, frobenius (ys t) = 1) ->
(forall x : 'cV_M, T x -> exists u : 'I_k.+1, frobenius (x - xs u) <= delta) ->
minmax (vec_mx (a *m bil_mx xs ys)) <=
escape_inf T (vec_mx a : 'M_(N, M)) + delta * frobenius a
Statement as written in the source
Lemma minmax_bil_le k l (xs : 'I_k.+1 -> 'cV[R]_M) (ys : 'I_l.+1 -> 'cV[R]_N)
    (delta : R) (a : 'rV[R]_(N * M)) :
  (forall t, frobenius (ys t) = 1) ->
  (forall x, T x -> exists u, frobenius (x - xs u) <= delta) ->
  minmax (vec_mx (a *m bil_mx xs ys)) <=
  escape_inf T (vec_mx a : 'M[R]_(N, M)) + delta * frobenius a.
Used by 1 declaration in 1 file
lemma rmax_fam_width source, line 613 
forall {R : realType} {M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
forall [k : nat] [xs : 'I_k.+1 -> 'cV_M] (h : 'rV_M),
(forall u : 'I_k.+1, T (xs u)) -> rmax (h *m fam_mx xs) <= gwidth_fun T h
Statement as written in the source
Lemma rmax_fam_width k (xs : 'I_k.+1 -> 'cV[R]_M) (h : 'rV[R]_M) :
  (forall u, T (xs u)) -> rmax (h *m fam_mx xs) <= gwidth_fun T h.
Used by 2 declarations in 1 file
theorem gordon_escape main result source, line 619 
forall {R : realType} {N M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
(0 < N)%N ->
\int[gauss N]_g frobenius g - \int[gauss M]_h gwidth_fun T h <=
\int[gauss (N * M)]_a escape_inf T (vec_mx a : 'M_(N, M))

Gordon's escape theorem: for the Gaussian matrix vec_mx a of size N x M, E[inf_(x in T) |vec_mx a *m x|] >= E[|g|] - E[sup_(x in T) <h, x>].

Main result, as the README states it

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

Used in theories/ by: Gordon/EscapeExpectation
Statement as written in the source
Theorem gordon_escape : (0 < N)%N ->
  \int[gauss N]_g frobenius g - \int[gauss M]_h gwidth_fun T h <=
  \int[gauss (N * M)]_a escape_inf T (vec_mx a : 'M[R]_(N, M)).
Used by 2 declarations in 1 file
theorem gordon_escape_tail main result source, line 700 
forall {R : realType} {N M : nat} [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
forall [u : R],
(0 < N)%N ->
0 <= u ->
(gauss (N * M)
   [set a | (escape_inf T (vec_mx a : 'M_(N, M)) <=
             \int[gauss N]_g frobenius g - \int[gauss M]_h gwidth_fun T h - u)%R] <=
 (expR (- u ^+ 2 / 2))%:E)%E

Escape through a mesh: inf_(x in T) |G x| falls below E[|g|] - E[sup_(x in T) <h, x>] - u with probability at most expR (- u^2 / 2).

Main result

Stated in the README together with gordon_escape.

Statement as written in the source
Theorem gordon_escape_tail (u : R) : (0 < N)%N -> 0 <= u ->
  (gauss (N * M) [set a | escape_inf T (vec_mx a : 'M[R]_(N, M)) <=
     \int[gauss N]_g frobenius g - \int[gauss M]_h gwidth_fun T h - u]%R <=
   (expR (- u ^+ 2 / 2))%:E)%E.
sectiongordon_minmax
Context {R : realType} {N M : nat}.
Variables (T : set 'cV[R]_M) (Y : set 'cV[R]_N).
Hypotheses (T1 : forall x, T x -> frobenius x = 1) (T0 : T !=set0).
Hypotheses (Y1 : forall y, Y y -> frobenius y = 1) (Y0 : Y !=set0).
definition minmax_sph source, line 729
Type
forall {R : realType} {N M : nat}, set 'cV_M -> set 'cV_N -> 'M_(N, M) -> R
Definition
Definition minmax_sph (G : 'M[R]_(N, M)) : R :=
  inf [set gwidth_fun Y (G *m x)^T | x in T].

inf_(x in T) sup_(y in Y) <y, G x>.

Used by 8 declarations in 1 file
let width_bound section-local source, line 732 
Let width_bound (v : 'rV[R]_N) : `|gwidth_fun Y v| <= frobenius v.
Used by 1 declaration in 1 file
lemma minmax_sph_le source, line 735 
forall {R : realType} {N M : nat} [T : set 'cV_M] [Y : set 'cV_N],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
(forall y : 'cV_N, Y y -> frobenius y = 1) ->
Y !=set0 ->
forall (G : 'M_(N, M)) [x : 'cV_M], T x -> minmax_sph T Y G <= gwidth_fun Y (G *m x)^T
Statement as written in the source
Lemma minmax_sph_le (G : 'M[R]_(N, M)) x :
  T x -> minmax_sph G <= gwidth_fun Y (G *m x)^T.
Used by 1 declaration in 1 file
lemma minmax_sph_ge source, line 746 
forall {R : realType} {N M : nat} [T : set 'cV_M] [Y : set 'cV_N],
T !=set0 ->
forall [G : 'M_(N, M)] [c : R],
(forall x : 'cV_M, T x -> c <= gwidth_fun Y (G *m x)^T) -> c <= minmax_sph T Y G
Statement as written in the source
Lemma minmax_sph_ge (G : 'M[R]_(N, M)) c :
  (forall x, T x -> c <= gwidth_fun Y (G *m x)^T) -> c <= minmax_sph G.
Used by 2 declarations in 1 file
lemma minmax_sph_lipschitz source, line 754 
forall {R : realType} {N M : nat} [T : set 'cV_M] [Y : set 'cV_N],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
(forall y : 'cV_N, Y y -> frobenius y = 1) ->
Y !=set0 ->
forall G G' : 'M_(N, M), `|minmax_sph T Y G - minmax_sph T Y G'| <= 1 * frobenius (G - G')
Statement as written in the source
Lemma minmax_sph_lipschitz (G G' : 'M[R]_(N, M)) :
  `|minmax_sph G - minmax_sph G'| <= 1 * frobenius (G - G').
Used by 1 declaration in 1 file
lemma integrable_minmax_sph source, line 772 
forall {R : realType} {N M : nat} [T : set 'cV_M] [Y : set 'cV_N],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
(forall y : 'cV_N, Y y -> frobenius y = 1) ->
Y !=set0 ->
(gauss (N * M)).-integrable [set: 'rV_(N * M)]
  (EFin \o (fun a : 'rV_(N * M) => minmax_sph T Y (vec_mx a : 'M_(N, M))))
Statement as written in the source
Lemma integrable_minmax_sph :
  (gauss (N * M)).-integrable [set: 'rV[R]_(N * M)]
    (EFin \o (fun a => minmax_sph (vec_mx a : 'M[R]_(N, M)))).
Used by 1 declaration in 1 file
lemma minmax_bil_sph_le source, line 781 
forall {R : realType} {N M : nat} [T : set 'cV_M] [Y : set 'cV_N],
T !=set0 ->
(forall y : 'cV_N, Y y -> frobenius y = 1) ->
Y !=set0 ->
forall [k l : nat] [xs : 'I_k.+1 -> 'cV_M] [ys : 'I_l.+1 -> 'cV_N] 
  [delta : R] (a : 'rV_(N * M)),
(forall t : 'I_l.+1, Y (ys t)) ->
(forall x : 'cV_M, T x -> exists u : 'I_k.+1, frobenius (x - xs u) <= delta) ->
minmax (vec_mx (a *m bil_mx xs ys)) <=
minmax_sph T Y (vec_mx a : 'M_(N, M)) + delta * frobenius a
Statement as written in the source
Lemma minmax_bil_sph_le k l (xs : 'I_k.+1 -> 'cV[R]_M)
    (ys : 'I_l.+1 -> 'cV[R]_N) (delta : R) (a : 'rV[R]_(N * M)) :
  (forall t, Y (ys t)) ->
  (forall x, T x -> exists u, frobenius (x - xs u) <= delta) ->
  minmax (vec_mx (a *m bil_mx xs ys)) <=
  minmax_sph (vec_mx a : 'M[R]_(N, M)) + delta * frobenius a.
Used by 1 declaration in 1 file
lemma rmax_net_width source, line 807 
forall {R : realType} {N : nat} [Y : set 'cV_N],
Y !=set0 ->
forall [l : nat] [ys : 'I_l.+1 -> 'cV_N] [eta : R] (g : 'rV_N),
(forall y : 'cV_N, Y y -> exists t : 'I_l.+1, frobenius (y - ys t) <= eta) ->
gwidth_fun Y g - eta * frobenius g <= rmax (g *m fam_mx ys)

If ys meets every ball of radius eta centered in Y, the largest of the <g, ys t> is at least sup_(y in Y) <g, y> - eta |g|.

Statement as written in the source
Lemma rmax_net_width l (ys : 'I_l.+1 -> 'cV[R]_N) (eta : R) (g : 'rV[R]_N) :
  (forall y, Y y -> exists t, frobenius (y - ys t) <= eta) ->
  gwidth_fun Y g - eta * frobenius g <= rmax (g *m fam_mx ys).
Used by 1 declaration in 1 file
theorem gordon_minmax main result source, line 825 
forall {R : realType} {N M : nat} [T : set 'cV_M] [Y : set 'cV_N],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
(forall y : 'cV_N, Y y -> frobenius y = 1) ->
Y !=set0 ->
\int[gauss N]_g gwidth_fun Y g - \int[gauss M]_h gwidth_fun T h <=
\int[gauss (N * M)]_a minmax_sph T Y (vec_mx a : 'M_(N, M))

Gordon's comparison for two sets of unit vectors: for the Gaussian matrix vec_mx a of size N x M, E[inf_(x in T) sup_(y in Y) <y, G x>] >= E[sup_(y in Y) <g, y>] - E[sup_(x in T) <h, x>].

Main result, as the README states it

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

Statement as written in the source
Theorem gordon_minmax :
  \int[gauss N]_g gwidth_fun Y g - \int[gauss M]_h gwidth_fun T h <=
  \int[gauss (N * M)]_a minmax_sph (vec_mx a : 'M[R]_(N, M)).
Used by 1 declaration in 1 file
sectiongordon_projection
Context {R : realType} {N M : nat}.
Variable P : 'M[R]_N.
Hypotheses (Psym : P^T = P) (Pid : P *m P = P) (P0 : P != 0).
Variable T : set 'cV[R]_M.
Hypotheses (T1 : forall x, T x -> frobenius x = 1) (T0 : T !=set0).
definition range_sphere source, line 923
Type
forall {R : realType} {N : nat}, 'M_N -> set 'cV_N
Definition
Definition range_sphere : set 'cV[R]_N :=
  [set y | frobenius y = 1 /\ P *m y = y].

The unit vectors of the range of the orthogonal projection P.

Used by 4 declarations in 1 file
lemma mxdot_proj source, line 926 
forall {R : realType} {N : nat} [P : 'M_N] (g : 'rV_N) [y : 'cV_N],
P *m y = y -> mxdot g^T y = mxdot (g *m P)^T y
Statement as written in the source
Lemma mxdot_proj (g : 'rV[R]_N) y :
  P *m y = y -> mxdot g^T y = mxdot (g *m P)^T y.
Used by 1 declaration in 1 file
lemma frobenius_proj_le source, line 932 
forall {R : realType} {N : nat} [P : 'M_N],
P^T = P ->
P *m P = P -> forall [m : nat] (A : 'M_(N, m)), frobenius (P *m A) <= frobenius A
Statement as written in the source
Lemma frobenius_proj_le m (A : 'M[R]_(N, m)) :
  frobenius (P *m A) <= frobenius A.
Used by 2 declarations in 1 file
lemma range_sphere0 source, line 940 
forall {R : realType} {N : nat} [P : 'M_N], P *m P = P -> P != 0 -> range_sphere P !=set0
Statement as written in the source
Lemma range_sphere0 : range_sphere !=set0.
Used by 2 declarations in 1 file
lemma gwidth_range_sphere source, line 953 
forall {R : realType} {N : nat} [P : 'M_N],
P^T = P ->
P *m P = P ->
P != 0 -> forall g : 'rV_N, gwidth_fun (range_sphere P) g = frobenius (g *m P)
Statement as written in the source
Lemma gwidth_range_sphere (g : 'rV[R]_N) :
  gwidth_fun range_sphere g = frobenius (g *m P).
Used by 2 declarations in 1 file
lemma minmax_sph_range source, line 980 
forall {R : realType} {N M : nat} [P : 'M_N],
P^T = P ->
P *m P = P ->
P != 0 ->
forall (T : set 'cV_M) (G : 'M_(N, M)),
minmax_sph T (range_sphere P) G = escape_inf T (P *m G)
Statement as written in the source
Lemma minmax_sph_range (G : 'M[R]_(N, M)) :
  minmax_sph T range_sphere G = escape_inf T (P *m G).
Used by 1 declaration in 1 file
theorem gordon_projection main result source, line 988 
forall {R : realType} {N M : nat} [P : 'M_N],
P^T = P ->
P *m P = P ->
P != 0 ->
forall [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
\int[gauss N]_g frobenius (g *m P) - \int[gauss M]_h gwidth_fun T h <=
\int[gauss (N * M)]_a escape_inf T (P *m vec_mx a : 'M_(N, M))

Gordon's comparison for P G: E[inf_(x in T) |P G x|] >= E[|g P|] - w(T).

Main result

Stated in the README together with gordon_minmax.

Statement as written in the source
Theorem gordon_projection :
  \int[gauss N]_g frobenius (g *m P) - \int[gauss M]_h gwidth_fun T h <=
  \int[gauss (N * M)]_a escape_inf T (P *m vec_mx a : 'M[R]_(N, M)).
Used by 1 declaration in 1 file
lemma escape_proj_lipschitz source, line 1004 
forall {R : realType} {N M : nat} [P : 'M_N],
P^T = P ->
P *m P = P ->
forall [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
forall a a' : 'rV_(N * M),
`|escape_inf T (P *m vec_mx a : 'M_(N, M)) - escape_inf T (P *m vec_mx a' : 'M_(N, M))| <=
1 * frobenius (a - a')
Statement as written in the source
Lemma escape_proj_lipschitz (a a' : 'rV[R]_(N * M)) :
  `|escape_inf T (P *m vec_mx a : 'M[R]_(N, M)) -
    escape_inf T (P *m vec_mx a' : 'M[R]_(N, M))| <=
  1 * frobenius (a - a').
Used by 2 declarations in 1 file
lemma measurable_escape_proj source, line 1014 
forall {R : realType} {N M : nat} [P : 'M_N],
P^T = P ->
P *m P = P ->
forall [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
forall [A : set R],
'measurable A ->
(measure_matrix_display default_measure_display).-measurable
  ((fun a : 'rV_(N * M) => escape_inf T (P *m vec_mx a : 'M_(N, M))) @^-1` A)
Statement as written in the source
Lemma measurable_escape_proj (A : set R) : measurable A ->
  measurable ((fun a : 'rV[R]_(N * M) =>
    escape_inf T (P *m vec_mx a : 'M[R]_(N, M))) @^-1` A).
Used by 2 declarations in 1 file
theorem gordon_projection_tail main result source, line 1023 
forall {R : realType} {N M : nat} [P : 'M_N],
P^T = P ->
P *m P = P ->
P != 0 ->
forall [T : set 'cV_M],
(forall x : 'cV_M, T x -> frobenius x = 1) ->
T !=set0 ->
forall [u : R],
0 <= u ->
(gauss (N * M)
   [set a | (escape_inf T (P *m vec_mx a : 'M_(N, M)) <=
             \int[gauss N]_g frobenius (g *m P) - \int[gauss M]_h gwidth_fun T h - u)%R] <=
 (expR (- u ^+ 2 / 2))%:E)%E
Main result

Stated in the README together with gordon_minmax.

Statement as written in the source
Theorem gordon_projection_tail (u : R) : 0 <= u ->
  (gauss (N * M) [set a | escape_inf T (P *m vec_mx a : 'M[R]_(N, M)) <=
     \int[gauss N]_g frobenius (g *m P) - \int[gauss M]_h gwidth_fun T h - u]%R
   <= (expR (- u ^+ 2 / 2))%:E)%E.
Used by 1 declaration in 1 file
sectionseq_index
lemma seq_index source, line 1039 
forall [T : eqType] (d : T) [x0 : T] [s : seq T] [y : T],
y \in x0 :: s -> exists t : 'I_(size s).+1, nth d (x0 :: s) t = y
Statement as written in the source
Lemma seq_index (T : eqType) (d x0 : T) (s : seq T) y : y \in x0 :: s ->
  exists t : 'I_(size s).+1, nth d (x0 :: s) t = y.
Used by 1 declaration in 1 file
sectionsymmetric_net
Context {R : realType} {n : nat}.
lemma sym_sphere_net source, line 1053 
forall {R : realType} {n : nat} [eps : R],
0 < eps ->
(0 < n)%N ->
exists (k : nat) (ys : 'I_k.+1 -> 'cV_n),
  [/\ forall t : 'I_k.+1, frobenius (ys t) = 1,
      forall t : 'I_k.+1, exists t' : 'I_k.+1, ys t' = - ys t
    & forall y : 'cV_n, frobenius y = 1 -> exists t : 'I_k.+1, frobenius (y - ys t) <= eps]

A symmetric eps-net of the unit sphere of 'cV[R]_n, as a family.

Statement as written in the source
Lemma sym_sphere_net (eps : R) : 0 < eps -> (0 < n)%N ->
  exists (k : nat) (ys : 'I_k.+1 -> 'cV[R]_n),
    [/\ forall t, frobenius (ys t) = 1,
        forall t, exists t', ys t' = - ys t &
        forall y, frobenius y = 1 -> exists t, frobenius (y - ys t) <= eps].
Used by 2 declarations in 2 files
sectiongauss_opnorm
Context {R : realType} {N M : nat}.
lemma opnorm_lipschitz source, line 1088 
forall {R : realType} {N M : nat} (A B : 'M_(N, M)),
`|opnorm A - opnorm B| <= frobenius (A - B)
Statement as written in the source
Lemma opnorm_lipschitz (A B : 'M[R]_(N, M)) :
  `|opnorm A - opnorm B| <= frobenius (A - B).
Used by 4 declarations in 3 files
lemma integrable_gauss_opnorm source, line 1098 
forall {R : realType} {N M : nat},
(gauss (N * M)).-integrable [set: 'rV_(N * M)]
  (EFin \o (fun a : 'rV_(N * M) => opnorm (vec_mx a : 'M_(N, M))))
Statement as written in the source
Lemma integrable_gauss_opnorm :
  (gauss (N * M)).-integrable [set: 'rV[R]_(N * M)]
    (EFin \o (fun a => opnorm (vec_mx a : 'M[R]_(N, M)))).
Used by 4 declarations in 3 files
theorem gauss_opnorm_mean main result source, line 1109 
forall {R : realType} {N M : nat},
(0 < N)%N ->
(0 < M)%N ->
\int[gauss (N * M)]_a opnorm (vec_mx a : 'M_(N, M)) <=
\int[gauss N]_g frobenius g + \int[gauss M]_h frobenius h

The operator norm of the N x M standard Gaussian matrix vec_mx a has mean at most E[|g|] + E[|h|], for g of law gauss N and h of law gauss M.

Main result, as the README states it

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

Statement as written in the source
Theorem gauss_opnorm_mean : (0 < N)%N -> (0 < M)%N ->
  \int[gauss (N * M)]_a opnorm (vec_mx a : 'M[R]_(N, M)) <=
  \int[gauss N]_g frobenius g + \int[gauss M]_h frobenius h.
Used by 3 declarations in 2 files
theorem gauss_opnorm_tail main result source, line 1178 
forall {R : realType} {N M : nat} [u : R],
(0 < N)%N ->
(0 < M)%N ->
0 <= u ->
(gauss (N * M)
   [set a | (\int[gauss N]_g frobenius g + \int[gauss M]_h frobenius h + u <=
             opnorm (vec_mx a : 'M_(N, M)))%R] <=
 (expR (- u ^+ 2 / 2))%:E)%E
Main result

Stated in the README together with gauss_opnorm_mean.

Statement as written in the source
Theorem gauss_opnorm_tail (u : R) : (0 < N)%N -> (0 < M)%N -> 0 <= u ->
  (gauss (N * M) [set a | \int[gauss N]_g frobenius g +
     \int[gauss M]_h frobenius h + u <= opnorm (vec_mx a : 'M[R]_(N, M))]%R <=
   (expR (- u ^+ 2 / 2))%:E)%E.
sectiongauss_frobenius_mean
Context {R : realType}.
lemma gauss_frobenius_mean_le main result source, line 1205 
forall {R : realType} (n : nat),
\int[gauss n]_g frobenius (g : 'rV_n) <= Num.ExtraDef.sqrtr n%:R

The mean Euclidean norm of a standard Gaussian vector of 'rV[R]_n is at most sqrt n.

Main result, as the README states it

E[|g|] <= sqrt n for g of law gauss n, and gauss n is invariant under x |-> - x.

Used in theories/ by: Gaussian/Symmetric/Reflection
Statement as written in the source
Lemma gauss_frobenius_mean_le n :
  \int[gauss n]_g frobenius (g : 'rV[R]_n) <= Num.sqrt n%:R.
Used by 5 declarations in 3 files
sectiongauss_matrix_bounds
Context {R : realType} {N M : nat}.
corollary gauss_opnorm_mean_sqrt main result source, line 1248 
forall {R : realType} {N M : nat},
(0 < N)%N ->
(0 < M)%N ->
\int[gauss (N * M)]_a opnorm (vec_mx a : 'M_(N, M)) <=
Num.ExtraDef.sqrtr N%:R + Num.ExtraDef.sqrtr M%:R
Main result

Stated in the README together with gauss_opnorm_mean.

Statement as written in the source
Corollary gauss_opnorm_mean_sqrt : (0 < N)%N -> (0 < M)%N ->
  \int[gauss (N * M)]_a opnorm (vec_mx a : 'M[R]_(N, M)) <=
  Num.sqrt N%:R + Num.sqrt M%:R.
Used by 2 declarations in 1 file
lemma gwidth_sphere main result source, line 1257 
forall {R : realType} {M : nat} (h : 'rV_M),
(0 < M)%N -> gwidth_fun (unit_sphere (n:=M)) h = frobenius h

The Gaussian width of the unit sphere of 'cV[R]_M is E[|h|].

Main result

Stated in the README together with gauss_min_singular_mean.

Statement as written in the source
Lemma gwidth_sphere (h : 'rV[R]_M) : (0 < M)%N ->
  gwidth_fun (@unit_sphere R M) h = frobenius h.
Used by 2 declarations in 1 file
corollary gauss_min_singular_mean main result source, line 1280 
forall {R : realType} {N M : nat},
(0 < N)%N ->
(0 < M)%N ->
\int[gauss N]_g frobenius g - \int[gauss M]_h frobenius h <=
\int[gauss (N * M)]_a escape_inf (unit_sphere (n:=M)) (vec_mx a : 'M_(N, M))

The smallest singular value: E[inf_(|x| = 1) |G x|] >= E[|g|] - E[|h|].

Main result, as the README states it

E[inf_(|x| = 1) |G x|] >= E[|g|] - E[|h|]: the Gaussian width of the unit sphere is E[|h|].

Statement as written in the source
Corollary gauss_min_singular_mean : (0 < N)%N -> (0 < M)%N ->
  \int[gauss N]_g frobenius g - \int[gauss M]_h frobenius h <=
  \int[gauss (N * M)]_a escape_inf (@unit_sphere R M) (vec_mx a : 'M[R]_(N, M)).
sectiongauss_projection_mean
Context {R : realType}.
lemma gauss_sqr_mulmx source, line 1301 
forall {R : realType} [n k : nat] (A : 'M_(n, k)),
\int[gauss n]_g frobenius (g *m A) ^+ 2 = frobenius A ^+ 2

E[|g A|^2] = |A|^2 for g of law gauss n.

Statement as written in the source
Lemma gauss_sqr_mulmx n k (A : 'M[R]_(n, k)) :
  \int[gauss n]_g frobenius (g *m A) ^+ 2 = frobenius A ^+ 2.
Used by 1 declaration in 1 file
lemma gauss_proj_mean_ge main result source, line 1343 
forall {R : realType} [n : nat] [P : 'M_n],
P^T = P ->
P *m P = P -> Num.ExtraDef.sqrtr (\tr P - 1) <= \int[gauss n]_g frobenius (g *m P)

For an orthogonal projection P, E[|g P|] >= sqrt (tr P - 1), by the Gaussian Poincare inequality, since E[|g P|^2] = tr P.

Main result

Stated in the README together with gordon_minmax.

Statement as written in the source
Lemma gauss_proj_mean_ge n (P : 'M[R]_n) : P^T = P -> P *m P = P ->
  Num.sqrt (\tr P - 1) <= \int[gauss n]_g frobenius (g *m P).
Used by 1 declaration in 1 file
sectiongauss_projection_singular
Context {R : realType} {N M : nat}.
theorem gauss_proj_singular_tail main result source, line 1407 
forall {R : realType} {N M : nat} [P : 'M_N] [u : R],
P^T = P ->
P *m P = P ->
P != 0 ->
(0 < M)%N ->
0 <= u ->
(gauss (N * M)
   [set a | (escape_inf (unit_sphere (n:=M)) (P *m vec_mx a : 'M_(N, M)) <=
             Num.ExtraDef.sqrtr (\tr P - 1) - Num.ExtraDef.sqrtr M%:R - u)%R] <=
 (expR (- u ^+ 2 / 2))%:E)%E

The smallest singular value of P G for an orthogonal projection P: inf_(|x| = 1) |P G x| is at most sqrt (tr P - 1) - sqrt M - u with probability at most expR (- u^2 / 2).

Main result

Stated in the README together with gordon_minmax.

Statement as written in the source
Theorem gauss_proj_singular_tail (P : 'M[R]_N) (u : R) :
  P^T = P -> P *m P = P -> P != 0 -> (0 < M)%N -> 0 <= u ->
  (gauss (N * M) [set a | escape_inf (@unit_sphere R M)
      (P *m vec_mx a : 'M[R]_(N, M)) <=
     Num.sqrt (\tr P - 1) - Num.sqrt M%:R - u]%R <=
   (expR (- u ^+ 2 / 2))%: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.