On this page

The convex Gaussian min-max theorem, in mean and concentration form

GaussianAnalysis.comparison.cgmtlibrary/comparison/cgmt.v1,590 lines53 lemmas and theorems, 7 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 1

GaussianAnalysis.comparison.cone_escape

Required by 7 files of the paper proofs

Theorem 5.3 of Koehler and Sohn (arXiv 2608.27372, lines 4972-4990; Thrampoulidis, Oymak and Hassibi, Theorem 3), in a self-contained form that suffices for the paper's limits. Let A be an N x M matrix of independent standard normal entries (A = vec_mx a, a of law gauss (N * M)) and g, h independent with laws gauss N and gauss M (g = lsubmx z and h = rsubmx z, z of law gauss (N + M)). For a nonempty set K of 'cV[R]_M with |x| <= rho on K, let

Phi(K) = inf_(x in K) |A x|                  (escape_inf K A, escape.v),
phi(K) = inf_(x in K) (|g| |x| - <h, x>)_+   (cgmt_aux K g h).

Then:

cgmt_lower: for N > 0, E Phi(K) >= E phi(K) - rho;
cgmt_upper: for K closed and convex, E Phi(K) <= E phi(K) + rho;
cgmt_escape_tail and cgmt_aux_tail: Phi(K) and phi(K) are at least u away from their means with probability at most 2 exp (- u^2 / (2 rho^2)) and 2 exp (- u^2 / (4 rho^2)) (gauss_concentration.v);
cgmt_tail: for N > 0 and K closed and convex, Phi(K) is at least rho + u away from E phi(K) with probability at most 2 exp (- u^2 / (2 rho^2)).

In the paper's application rho is O(d) while Phi and phi are normalized by d^(3/2), so the error rho vanishes: the normalized Phi and phi have the same limit in probability, which is what the comparisons (eq:cgmt-comparisons) of the paper are used for.

cgmt_aux_mean_zero, cgmt_zero_tail: if phi(K) vanishes with probability more than 1/2, then E phi(K) <= 2 rho sqrt (ln 4), and Phi(K) exceeds rho (1 + 2 sqrt (ln 4)) + u with probability at most 2 exp (- u^2 / (2 rho^2)): the approximate solutions that the CGMT gives when the auxiliary problem has the value 0.
measurable_escape_inf, measurable_cgmt_aux: Phi(K) and phi(K) are measurable functions of the Gaussian entries (they are Lipschitz), so that their laws are defined.
For a set K of row vectors, the theorems apply to the set tr_set K of their transposes: escape_inf_tr_set and cgmt_aux_tr_set write Phi and phi as infima over K, and tr_set K is nonempty, bounded, closed or convex with K (tr_set_neq0, tr_set_bounded, closed_tr_set, convex_tr_set).

The proofs. gordon_gamma is Gordon's inequality (gordon.v) for finite families rs u and cs t: the min-max over u and t of |rs u| <g, cs t> + |cs t| <h, rs u> is in mean at most that of the bilinear process plus gamma |rs u| |cs t|, gamma an independent standard normal. infsup_compare extends it to bounded index sets by eps-nets (nets.v). The lower bound takes the index sets K and the unit ball, where sup_(|y| <= 1) (|x| <g, y> + |y| <h, x>) = (|g| |x| + <h, x>)_+; the term in gamma costs at most E |gamma| rho <= rho, and the sign of h changes by the symmetry of gauss. The upper bound exchanges the index sets and uses the minimax exchange escape_inf_minimax: for K closed and convex, inf_(x in K) |A x| <= sup_(|y| <= 1) inf_(x in K) <y, A x>, by the variational inequality at a minimizer of |A x| on the compact set K (closed_bounded_compact_cV).

`cgmt_aux K g h`	inf_(x in K) (\|g\| \|x\| - <h, x>)_+
`tr_set K`	the set of the transposes x^T of the x in K
`infsup S T F`	inf_(s in S) sup_(t in T) F s t
`auxg_mx rs cs`	the matrix C such that vec_mx (z *m C) u t is \|rs u\| <lsubmx z, cs t> + \|cs t\| <rsubmx z, rs u>
`auxgT_mx rs cs`	the same with the two blocks of z exchanged
`bilg_mx rs cs B`	the matrix C such that vec_mx (w m C) u t is vec_mx (lsubmx w m B) u t + rsubmx w 0 0 \|rs u\| \|cs t\|

Main results

Results	Statement
cgmt_lowercgmt_uppercgmt_aux	The convex Gaussian min-max theorem in mean form (Theorem 5.3 of Koehler and Sohn; Thrampoulidis, Oymak and Hassibi, Theorem 3): let `A = vec_mx a` be an `N x M` matrix of independent standard normal entries, `z = (g, h)` of law `gauss (N + M)`, and `K` a nonempty set of `'cV[R]_M` with `\|x\| <= rho` on `K`; let `Phi(K) = inf_(x in K) \|A x\|` (`escape_inf`) and `phi(K) = inf_(x in K) (\|g\| \|x\| - <h, x>)_+` (`cgmt_aux`). Then `E Phi(K) >= E phi(K) - rho` for `N > 0`, and `E Phi(K) <= E phi(K) + rho` for `K` closed and convex.
cgmt_escape_tailcgmt_aux_tailcgmt_tail	`Phi(K)` is `rho`-Lipschitz in `a` and `phi(K)` is `sqrt 2 rho`-Lipschitz in `z`, so they are at least `u` away from their means with probability at most `2 exp (- u^2 / (2 rho^2))` and `2 exp (- u^2 / (4 rho^2))`. For `N > 0` and `K` closed and convex, `Phi(K)` is at least `rho + u` away from `E phi(K)` with probability at most `2 exp (- u^2 / (2 rho^2))`.
gordon_gammainfsup_compareescape_inf_minimaxclosed_bounded_compact_cV	Gordon's comparison of `\|x\| <g, y> + \|y\| <h, x>` with `y^T A x + gamma \|x\| \|y\|`, `gamma` an independent standard normal, for finite families and, by nets, as `E inf_(s in S) sup_(t in T)` inequalities for bounded index sets; the minimax exchange `inf_(x in K) \|A x\| <= sup_(\|y\| <= 1) inf_(x in K) <y, A x>` for `K` closed, bounded and convex; closed bounded sets of column vectors are compact.
measurable_escape_infmeasurable_cgmt_auxtr_setescape_inf_tr_setcgmt_aux_tr_set	`Phi(K)` and `phi(K)` are measurable functions of the Gaussian entries, so that their laws are defined. For a set `K` of row vectors, the theorems apply to the set `tr_set K` of the transposes, with `Phi = inf_(x in K) \|A x^T\|` and `phi = inf_(x in K) (\|g\| \|x\| - <h, x>)_+`; `tr_set K` is nonempty, bounded, closed or convex with `K`.
cgmt_aux_mean_zerocgmt_zero_tail	If `phi(K)` vanishes with probability more than `1/2`, then `E phi(K) <= 2 rho sqrt (ln 4)` (concentration), and `Phi(K) >= rho (1 + 2 sqrt (ln 4)) + u` has probability at most `2 exp (- u^2 / (2 rho^2))`: the approximate solutions of `A x = 0` on `K` that the CGMT gives when the auxiliary problem has the value `0`.

Declarations60 exported, 26 local

sectiongordon_gamma

Context {R : realType} {P Q k l : nat}.
Variables (rs : 'I_k.+1 -> 'cV[R]_P) (cs : 'I_l.+1 -> 'cV[R]_Q).
Local Notation idx := (@mxvec_index k.+1 l.+1).

definition nrm_mx source, line 99

Type

forall {R : realType} {P Q k l : nat},
('I_k.+1 -> 'cV_P) -> ('I_l.+1 -> 'cV_Q) -> 'rV_(k.+1 * l.+1)

Definition

Definition nrm_mx : 'M[R]_(1, k.+1 * l.+1) :=
  \matrix_(i, c) (frobenius (rs (unvec c).1) * frobenius (cs (unvec c).2)).

The row of the term gamma |rs u| |cs t|.

Used by 3 declarations in 1 file

this file: nrm_cov, bilg_mx, incr_var_gamma

definition auxg_mx source, line 104

Type

forall {R : realType} {P Q k l : nat},
('I_k.+1 -> 'cV_P) -> ('I_l.+1 -> 'cV_Q) -> 'M_(Q + P, k.+1 * l.+1)

Definition

Definition auxg_mx : 'M[R]_(Q + P, k.+1 * l.+1) :=
  col_mx (\matrix_(i, c) (frobenius (rs (unvec c).1) * cs (unvec c).2 i 0))
         (\matrix_(j, c) (frobenius (cs (unvec c).2) * rs (unvec c).1 j 0)).

For z of law gauss (Q + P), the Gaussian matrix whose entry (u, t) is |rs u| <lsubmx z, cs t> + |cs t| <rsubmx z, rs u>.

Used by 3 declarations in 1 file

this file: auxg_mxE, auxg_cov, XY_low

lemma auxg_mxE source, line 108

forall {R : realType} {P Q k l : nat} (rs : 'I_k.+1 -> 'cV_P) (cs : 'I_l.+1 -> 'cV_Q)
  (z : 'rV_(Q + P)) (u : 'I_k.+1) (t : 'I_l.+1),
vec_mx (z *m auxg_mx rs cs) u t =
frobenius (rs u) * mxdot (lsubmx z)^T (cs t) + frobenius (cs t) * mxdot (rsubmx z)^T (rs u)

Statement as written in the source

Lemma auxg_mxE (z : 'rV[R]_(Q + P)) u t :
  vec_mx (z *m auxg_mx) u t =
  frobenius (rs u) * mxdot (lsubmx z)^T (cs t) +
  frobenius (cs t) * mxdot (rsubmx z)^T (rs u).

Used by 1 declaration in 1 file

this file: XY_low

lemma auxg_cov source, line 121

forall {R : realType} {P Q k l : nat} (rs : 'I_k.+1 -> 'cV_P) (cs : 'I_l.+1 -> 'cV_Q)
  (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
((auxg_mx rs cs)^T *m auxg_mx rs cs) (mxvec_index u t) (mxvec_index v s) =
frobenius (rs u) * frobenius (rs v) * mxdot (cs t) (cs s) +
frobenius (cs t) * frobenius (cs s) * mxdot (rs u) (rs v)

Statement as written in the source

Lemma auxg_cov u t v s :
  (auxg_mx^T *m auxg_mx) (idx u t) (idx v s) =
  frobenius (rs u) * frobenius (rs v) * mxdot (cs t) (cs s) +
  frobenius (cs t) * frobenius (cs s) * mxdot (rs u) (rs v).

Used by 1 declaration in 1 file

this file: XY_low

definition auxgT_mx source, line 137

Type

forall {R : realType} {P Q k l : nat},
('I_k.+1 -> 'cV_P) -> ('I_l.+1 -> 'cV_Q) -> 'M_(P + Q, k.+1 * l.+1)

Definition

Definition auxgT_mx : 'M[R]_(P + Q, k.+1 * l.+1) :=
  col_mx (\matrix_(j, c) (frobenius (cs (unvec c).2) * rs (unvec c).1 j 0))
         (\matrix_(i, c) (frobenius (rs (unvec c).1) * cs (unvec c).2 i 0)).

The same process with the blocks of z in the other order: for z of law gauss (P + Q), the entry (u, t) is |cs t| <lsubmx z, rs u> + |rs u| <rsubmx z, cs t>.

Used by 3 declarations in 1 file

this file: auxgT_mxE, auxgT_cov, XY_up

lemma auxgT_mxE source, line 141

forall {R : realType} {P Q k l : nat} (rs : 'I_k.+1 -> 'cV_P) (cs : 'I_l.+1 -> 'cV_Q)
  (z : 'rV_(P + Q)) (u : 'I_k.+1) (t : 'I_l.+1),
vec_mx (z *m auxgT_mx rs cs) u t =
frobenius (cs t) * mxdot (lsubmx z)^T (rs u) + frobenius (rs u) * mxdot (rsubmx z)^T (cs t)

Statement as written in the source

Lemma auxgT_mxE (z : 'rV[R]_(P + Q)) u t :
  vec_mx (z *m auxgT_mx) u t =
  frobenius (cs t) * mxdot (lsubmx z)^T (rs u) +
  frobenius (rs u) * mxdot (rsubmx z)^T (cs t).

Used by 1 declaration in 1 file

this file: XY_up

lemma auxgT_cov source, line 154

forall {R : realType} {P Q k l : nat} (rs : 'I_k.+1 -> 'cV_P) (cs : 'I_l.+1 -> 'cV_Q)
  (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
((auxgT_mx rs cs)^T *m auxgT_mx rs cs) (mxvec_index u t) (mxvec_index v s) =
frobenius (rs u) * frobenius (rs v) * mxdot (cs t) (cs s) +
frobenius (cs t) * frobenius (cs s) * mxdot (rs u) (rs v)

Statement as written in the source

Lemma auxgT_cov u t v s :
  (auxgT_mx^T *m auxgT_mx) (idx u t) (idx v s) =
  frobenius (rs u) * frobenius (rs v) * mxdot (cs t) (cs s) +
  frobenius (cs t) * frobenius (cs s) * mxdot (rs u) (rs v).

Used by 1 declaration in 1 file

this file: XY_up

lemma nrm_cov source, line 167

forall {R : realType} {P Q k l : nat} (rs : 'I_k.+1 -> 'cV_P) (cs : 'I_l.+1 -> 'cV_Q)
  (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
((nrm_mx rs cs)^T *m nrm_mx rs cs) (mxvec_index u t) (mxvec_index v s) =
frobenius (rs u) * frobenius (cs t) * (frobenius (rs v) * frobenius (cs s))

Statement as written in the source

Lemma nrm_cov u t v s :
  (nrm_mx^T *m nrm_mx) (idx u t) (idx v s) =
  frobenius (rs u) * frobenius (cs t) * (frobenius (rs v) * frobenius (cs s)).

Used by 1 declaration in 1 file

this file: incr_var_gamma

Variables (n : nat) (Bm : 'M[R]_(n, k.+1 * l.+1)).
Hypothesis Bcov : forall u t v s,
  (Bm^T *m Bm) (idx u t) (idx v s) = mxdot (rs u) (rs v) * mxdot (cs t) (cs s).

definition bilg_mx source, line 178

Type

forall {R : realType} {P Q k l : nat},
('I_k.+1 -> 'cV_P) ->
('I_l.+1 -> 'cV_Q) -> forall [n : nat], 'M_(n, k.+1 * l.+1) -> 'M_(n + 1, k.+1 * l.+1)

Definition

Definition bilg_mx : 'M[R]_(n + 1, k.+1 * l.+1) := col_mx Bm nrm_mx.

The bilinear process plus gamma |rs u| |cs t|, gamma the last coordinate of a vector of law gauss (n + 1).

Used by 5 declarations in 1 file

this file: bilg_mxE, incr_var_gamma, gordon_gamma, XY_low, XY_up

lemma bilg_mxE source, line 180

forall {R : realType} {P Q k l : nat} (rs : 'I_k.+1 -> 'cV_P) (cs : 'I_l.+1 -> 'cV_Q)
  [n : nat] (Bm : 'M_(n, k.+1 * l.+1)) (w : 'rV_(n + 1)) (u : 'I_k.+1) 
  (t : 'I_l.+1),
vec_mx (w *m bilg_mx rs cs Bm) u t =
vec_mx (lsubmx w *m Bm) u t + rsubmx w 0 0 * (frobenius (rs u) * frobenius (cs t))

Statement as written in the source

Lemma bilg_mxE (w : 'rV[R]_(n + 1)) u t :
  vec_mx (w *m bilg_mx) u t = vec_mx (lsubmx w *m Bm) u t +
    rsubmx w 0 0 * (frobenius (rs u) * frobenius (cs t)).

Used by 2 declarations in 1 file

this file: XY_low, XY_up

C is auxg_mx or auxgT_mx: only its covariance matters.

Variables (m : nat) (C : 'M[R]_(m, k.+1 * l.+1)).
Hypothesis Ccov : forall u t v s,
  (C^T *m C) (idx u t) (idx v s) =
  frobenius (rs u) * frobenius (rs v) * mxdot (cs t) (cs s) +
  frobenius (cs t) * frobenius (cs s) * mxdot (rs u) (rs v).

lemma incr_var_gamma source, line 196

forall {R : realType} {P Q k l : nat} [rs : 'I_k.+1 -> 'cV_P] [cs : 'I_l.+1 -> 'cV_Q]
  [n : nat] [Bm : 'M_(n, k.+1 * l.+1)],
(forall (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
 (Bm^T *m Bm) (mxvec_index u t) (mxvec_index v s) =
 mxdot (rs u) (rs v) * mxdot (cs t) (cs s)) ->
forall [m : nat] [C : 'M_(m, k.+1 * l.+1)],
(forall (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
 (C^T *m C) (mxvec_index u t) (mxvec_index v s) =
 frobenius (rs u) * frobenius (rs v) * mxdot (cs t) (cs s) +
 frobenius (cs t) * frobenius (cs s) * mxdot (rs u) (rs v)) ->
forall (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
incr_var C (mxvec_index u t) (mxvec_index v s) -
incr_var (bilg_mx rs cs Bm) (mxvec_index u t) (mxvec_index v s) =
2 * (frobenius (rs u) * frobenius (rs v) - mxdot (rs u) (rs v)) *
(frobenius (cs t) * frobenius (cs s) - mxdot (cs t) (cs s))

Statement as written in the source

Lemma incr_var_gamma u t v s :
  incr_var C (idx u t) (idx v s) - incr_var bilg_mx (idx u t) (idx v s) =
  2 * (frobenius (rs u) * frobenius (rs v) - mxdot (rs u) (rs v)) *
      (frobenius (cs t) * frobenius (cs s) - mxdot (cs t) (cs s)).

Used by 1 declaration in 1 file

this file: gordon_gamma

lemma gordon_gamma main result source, line 210

forall {R : realType} {P Q k l : nat} [rs : 'I_k.+1 -> 'cV_P] [cs : 'I_l.+1 -> 'cV_Q]
  [n : nat] [Bm : 'M_(n, k.+1 * l.+1)],
(forall (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
 (Bm^T *m Bm) (mxvec_index u t) (mxvec_index v s) =
 mxdot (rs u) (rs v) * mxdot (cs t) (cs s)) ->
forall [m : nat] [C : 'M_(m, k.+1 * l.+1)],
(forall (u : 'I_k.+1) (t : 'I_l.+1) (v : 'I_k.+1) (s : 'I_l.+1),
 (C^T *m C) (mxvec_index u t) (mxvec_index v s) =
 frobenius (rs u) * frobenius (rs v) * mxdot (cs t) (cs s) +
 frobenius (cs t) * frobenius (cs s) * mxdot (rs u) (rs v)) ->
(\int[gauss m]_z (minmax (vec_mx (z *m C)))%:E <=
 \int[gauss (n + 1)]_w (minmax (vec_mx (w *m bilg_mx rs cs Bm)))%:E)%E

Gordon's comparison of the auxiliary process with the bilinear process plus gamma |rs u| |cs t|.

Main result, as the README states it

Gordon's comparison of |x| <g, y> + |y| <h, x> with y^T A x + gamma |x| |y|, gamma an independent standard normal, for finite families and, by nets, as E inf_(s in S) sup_(t in T) inequalities for bounded index sets; the minimax exchange inf_(x in K) |A x| <= sup_(|y| <= 1) inf_(x in K) <y, A x> for K closed, bounded and convex; closed bounded sets of column vectors are compact.

Statement as written in the source

Lemma gordon_gamma :
  (\int[gauss m]_z (minmax (vec_mx (z *m C)))%:E <=
   \int[gauss (n + 1)]_w (minmax (vec_mx (w *m bilg_mx)))%:E)%E.

Used by 2 declarations in 1 file

this file: XY_low, XY_up

sectioninfsup

Context {R : realType} {P Q : nat}.
Variables (S : set 'cV[R]_P) (T : set 'cV[R]_Q).
Hypotheses (S0 : S !=set0) (T0 : T !=set0).
Implicit Types (F G : 'cV[R]_P -> 'cV[R]_Q -> R) (B L e : R).

definition infsup source, line 230

Type

forall {R : realType} {P Q : nat}, set 'cV_P -> set 'cV_Q -> ('cV_P -> 'cV_Q -> R) -> R

Definition

Definition infsup F : R := inf [set sup [set F s t | t in T] | s in S].

inf_(s in S) sup_(t in T) F s t.

Used by 15 declarations in 1 file

this file: infsup_le, le_infsup, infsup_bound, infsup_lipschitz, infsup_net, integrable_infsupX, integrable_infsupY, infsup_compare, escape_inf_minimax, low_aux, low_X, cgmt_lower, up_X, up_Y, cgmt_upper

sectionbounded

Variables (F : 'cV[R]_P -> 'cV[R]_Q -> R) (B : R).
Hypothesis FB : forall s t, S s -> T t -> `|F s t| <= B.

lemma sup_row_ub source, line 236

forall {R : realType} {P Q : nat} [S0 : set 'cV_P] [T : set 'cV_Q]
  [F : 'cV_P -> 'cV_Q -> R] [B : R],
(forall (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|F s t| <= B) ->
forall [s : 'cV_P] [t : 'cV_Q], S0 s -> T t -> F s t <= sup [set F s t0 | t0 in T]

Statement as written in the source

Lemma sup_row_ub s t : S s -> T t -> F s t <= sup [set F s t | t in T].

Used by 5 declarations in 1 file

this file: sup_row_bound, infsup_lipschitz, infsup_net, low_aux, up_Y

lemma sup_row_le source, line 242

forall {R : realType} {P Q : nat} [S0 : set 'cV_P] [T : set 'cV_Q],
T !=set0 ->
forall [F : 'cV_P -> 'cV_Q -> R] [s : 'cV_P] [c : R],
S0 s -> (forall t : 'cV_Q, T t -> F s t <= c) -> sup [set F s t | t in T] <= c

Statement as written in the source

Lemma sup_row_le s c : S s -> (forall t, T t -> F s t <= c) ->
  sup [set F s t | t in T] <= c.

Used by 5 declarations in 1 file

this file: sup_row_bound, infsup_lipschitz, infsup_net, escape_inf_minimax, low_X

lemma sup_row_bound source, line 249

forall {R : realType} {P Q : nat} [S0 : set 'cV_P] [T : set 'cV_Q],
T !=set0 ->
forall [F : 'cV_P -> 'cV_Q -> R] [B : R],
(forall (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|F s t| <= B) ->
forall [s : 'cV_P], S0 s -> `|sup [set F s t | t in T]| <= B

Statement as written in the source

Lemma sup_row_bound s : S s -> `|sup [set F s t | t in T]| <= B.

Used by 2 declarations in 1 file

this file: infsup_le, infsup_bound

lemma infsup_le source, line 258

forall {R : realType} {P Q : nat} [S0 : set 'cV_P] [T : set 'cV_Q],
T !=set0 ->
forall [F : 'cV_P -> 'cV_Q -> R] [B : R],
(forall (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|F s t| <= B) ->
forall [s : 'cV_P], S0 s -> infsup S0 T F <= sup [set F s t | t in T]

Statement as written in the source

Lemma infsup_le s : S s -> infsup F <= sup [set F s t | t in T].

Used by 5 declarations in 1 file

this file: infsup_bound, infsup_lipschitz, infsup_net, escape_inf_minimax, low_X

lemma le_infsup source, line 265

forall {R : realType} {P Q : nat} [S0 : set 'cV_P] [T : set 'cV_Q],
S0 !=set0 ->
forall [F : 'cV_P -> 'cV_Q -> R] [c : R],
(forall s : 'cV_P, S0 s -> c <= sup [set F s t | t in T]) -> c <= infsup S0 T F

Statement as written in the source

Lemma le_infsup c : (forall s, S s -> c <= sup [set F s t | t in T]) ->
  c <= infsup F.

Used by 5 declarations in 1 file

this file: infsup_bound, infsup_lipschitz, infsup_net, low_aux, up_Y

lemma infsup_bound source, line 273

forall {R : realType} {P Q : nat} [S0 : set 'cV_P] [T : set 'cV_Q],
S0 !=set0 ->
T !=set0 ->
forall [F : 'cV_P -> 'cV_Q -> R] [B : R],
(forall (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|F s t| <= B) -> `|infsup S0 T F| <= B

Statement as written in the source

Lemma infsup_bound : `|infsup F| <= B.

lemma infsup_lipschitz source, line 286

forall {R : realType} {P Q : nat} [S0 : set 'cV_P] [T : set 'cV_Q],
S0 !=set0 ->
T !=set0 ->
forall [F G : 'cV_P -> 'cV_Q -> R] [B : R]
  [c : {|
         Num.POrderZmodule.sort := R;
         Num.POrderZmodule.class :=
           {|
             Num.POrderZmodule.choice_hasChoice_mixin := Real.class R;
             Num.POrderZmodule.eqtype_hasDecEq_mixin := Real.class R;
             Num.POrderZmodule.Order_isDuallyPreorder_mixin := Real.class R;
             Num.POrderZmodule.Order_Preorder_isDuallyPOrder_mixin := Real.class R;
             Num.POrderZmodule.Algebra_hasOpp_mixin := Real.class R;
             Num.POrderZmodule.Algebra_hasZero_mixin := Real.class R;
             Num.POrderZmodule.Algebra_hasAdd_mixin := Real.class R;
             Num.POrderZmodule.Algebra_BaseZmoduleNmodule_isZmodule_mixin := Real.class R;
             Num.POrderZmodule.Algebra_BaseAddUMagma_isAddUMagma_mixin := Real.class R;
             Num.POrderZmodule.Algebra_BaseAddMagma_isAddMagma_mixin := Real.class R;
             Num.POrderZmodule.Algebra_AddMagma_isAddSemigroup_mixin := Real.class R
           |}
       |}],
(forall (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|F s t| <= B) ->
(forall (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|G s t| <= B) ->
(forall (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|F s t - G s t| <= c) ->
`|infsup S0 T F - infsup S0 T G| <= c

infsup is 1-Lipschitz for the uniform distance on S x T.

Statement as written in the source

Lemma infsup_lipschitz F G B c :
  (forall s t, S s -> T t -> `|F s t| <= B) ->
  (forall s t, S s -> T t -> `|G s t| <= B) ->
  (forall s t, S s -> T t -> `|F s t - G s t| <= c) ->
  `|infsup F - infsup G| <= c.

Used by 3 declarations in 1 file

this file: integrable_infsupX, integrable_infsupY, up_X

lemma infsup_net source, line 314

forall {R : realType} {P Q : nat} [S0 : set 'cV_P] [T : set 'cV_Q],
S0 !=set0 ->
T !=set0 ->
forall [k l : nat] [rs : 'I_k.+1 -> 'cV_P] [cs : 'I_l.+1 -> 'cV_Q]
  [F : 'cV_P -> 'cV_Q -> R] [B L e : R],
0 <= L ->
(forall (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|F s t| <= B) ->
(forall u : 'I_k.+1, S0 (rs u)) ->
(forall t : 'I_l.+1, T (cs t)) ->
(forall s : 'cV_P, S0 s -> exists u : 'I_k.+1, frobenius (s - rs u) <= e) ->
(forall t : 'cV_Q, T t -> exists v : 'I_l.+1, frobenius (t - cs v) <= e) ->
(forall (s s' : 'cV_P) (t : 'cV_Q),
 S0 s -> S0 s' -> T t -> `|F s t - F s' t| <= L * frobenius (s - s')) ->
(forall (s : 'cV_P) (t t' : 'cV_Q),
 S0 s -> T t -> T t' -> `|F s t - F s t'| <= L * frobenius (t - t')) ->
`|minmax (\matrix_(u, v) F (rs u) (cs v)) - infsup S0 T F| <= L * e

Nets: if every point of S is within e of some rs u, every point of T within e of some cs t, and F is L-Lipschitz in each variable, the finite min-max is within L e of infsup F.

Statement as written in the source

Lemma infsup_net k l (rs : 'I_k.+1 -> 'cV[R]_P) (cs : 'I_l.+1 -> 'cV[R]_Q)
    F B L e : 0 <= L ->
  (forall s t, S s -> T t -> `|F s t| <= B) ->
  (forall u, S (rs u)) -> (forall t, T (cs t)) ->
  (forall s, S s -> exists u, frobenius (s - rs u) <= e) ->
  (forall t, T t -> exists v, frobenius (t - cs v) <= e) ->
  (forall s s' t, S s -> S s' -> T t ->
     `|F s t - F s' t| <= L * frobenius (s - s')) ->
  (forall s t t', S s -> T t -> T t' ->
     `|F s t - F s t'| <= L * frobenius (t - t')) ->
  `|minmax (\matrix_(u, v) F (rs u) (cs v)) - infsup F| <= L * e.

Used by 1 declaration in 1 file

this file: infsup_compare

sectioninfsup_compare

Context {R : realType} {P Q m1 m2 : nat}.
Variables (S : set 'cV[R]_P) (T : set 'cV[R]_Q) (rhoS rhoT c : R).
Hypotheses (S0 : S !=set0) (T0 : T !=set0).
Hypotheses (Sb : forall s, S s -> frobenius s <= rhoS)
  (Tb : forall t, T t -> frobenius t <= rhoT).
Variables (X : 'rV[R]_m1 -> 'cV[R]_P -> 'cV[R]_Q -> R)
  (Y : 'rV[R]_m2 -> 'cV[R]_P -> 'cV[R]_Q -> R).
Hypothesis c0 : 0 <= c.

X and Y are bounded, Lipschitz in the index and in the Gaussian vector

Hypothesis Xb : forall w s t, S s -> T t -> `|X w s t| <= c * frobenius w.
Hypothesis Yb : forall z s t, S s -> T t -> `|Y z s t| <= c * frobenius z.
Hypothesis Xs : forall w s s' t, S s -> S s' -> T t ->
  `|X w s t - X w s' t| <= c * frobenius w * frobenius (s - s').
Hypothesis Xt : forall w s t t', S s -> T t -> T t' ->
  `|X w s t - X w s t'| <= c * frobenius w * frobenius (t - t').
Hypothesis Ys : forall z s s' t, S s -> S s' -> T t ->
  `|Y z s t - Y z s' t| <= c * frobenius z * frobenius (s - s').
Hypothesis Yt : forall z s t t', S s -> T t -> T t' ->
  `|Y z s t - Y z s t'| <= c * frobenius z * frobenius (t - t').
Hypothesis Xw : forall w w' s t, S s -> T t ->
  `|X w s t - X w' s t| <= c * frobenius (w - w').
Hypothesis Yz : forall z z' s t, S s -> T t ->
  `|Y z s t - Y z' s t| <= c * frobenius (z - z').

the comparison for finite families

Hypothesis XY : forall k l (rs : 'I_k.+1 -> 'cV[R]_P)
    (cs : 'I_l.+1 -> 'cV[R]_Q), (forall u, S (rs u)) -> (forall t, T (cs t)) ->
  (\int[gauss m2]_z (minmax (\matrix_(u, t) Y z (rs u) (cs t)))%:E <=
   \int[gauss m1]_w (minmax (\matrix_(u, t) X w (rs u) (cs t)))%:E)%E.

lemma integrable_infsupX source, line 387

forall {R : realType} {P Q m1 : nat} [S0 : set 'cV_P] [T : set 'cV_Q] [c : R],
S0 !=set0 ->
T !=set0 ->
forall [X : 'rV_m1 -> 'cV_P -> 'cV_Q -> R],
0 <= c ->
(forall (w : 'rV_m1) (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|X w s t| <= c * frobenius w) ->
(forall (w w' : 'rV_m1) (s : 'cV_P) (t : 'cV_Q),
 S0 s -> T t -> `|X w s t - X w' s t| <= c * frobenius (w - w')) ->
(gauss m1).-integrable [set: 'rV_m1] (EFin \o (fun w : 'rV_m1 => infsup S0 T (X w)))

Statement as written in the source

Lemma integrable_infsupX :
  (gauss m1).-integrable setT (EFin \o (fun w => infsup S T (X w))).

Used by 3 declarations in 1 file

this file: infsup_compare, cgmt_lower, cgmt_upper

lemma integrable_infsupY source, line 400

forall {R : realType} {P Q m2 : nat} [S0 : set 'cV_P] [T : set 'cV_Q] [c : R],
S0 !=set0 ->
T !=set0 ->
forall [Y : 'rV_m2 -> 'cV_P -> 'cV_Q -> R],
0 <= c ->
(forall (z : 'rV_m2) (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|Y z s t| <= c * frobenius z) ->
(forall (z z' : 'rV_m2) (s : 'cV_P) (t : 'cV_Q),
 S0 s -> T t -> `|Y z s t - Y z' s t| <= c * frobenius (z - z')) ->
(gauss m2).-integrable [set: 'rV_m2] (EFin \o (fun z : 'rV_m2 => infsup S0 T (Y z)))

Statement as written in the source

Lemma integrable_infsupY :
  (gauss m2).-integrable setT (EFin \o (fun z => infsup S T (Y z))).

Used by 3 declarations in 1 file

this file: infsup_compare, cgmt_lower, cgmt_upper

theorem infsup_compare main result source, line 414

forall {R : realType} {P Q m1 m2 : nat} [S0 : set 'cV_P] [T : set 'cV_Q] [rhoS rhoT c : R],
S0 !=set0 ->
T !=set0 ->
(forall s : 'cV_P, S0 s -> frobenius s <= rhoS) ->
(forall t : 'cV_Q, T t -> frobenius t <= rhoT) ->
forall [X : 'rV_m1 -> 'cV_P -> 'cV_Q -> R] [Y : 'rV_m2 -> 'cV_P -> 'cV_Q -> R],
0 <= c ->
(forall (w : 'rV_m1) (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|X w s t| <= c * frobenius w) ->
(forall (z : 'rV_m2) (s : 'cV_P) (t : 'cV_Q), S0 s -> T t -> `|Y z s t| <= c * frobenius z) ->
(forall (w : 'rV_m1) (s s' : 'cV_P) (t : 'cV_Q),
 S0 s -> S0 s' -> T t -> `|X w s t - X w s' t| <= c * frobenius w * frobenius (s - s')) ->
(forall (w : 'rV_m1) (s : 'cV_P) (t t' : 'cV_Q),
 S0 s -> T t -> T t' -> `|X w s t - X w s t'| <= c * frobenius w * frobenius (t - t')) ->
(forall (z : 'rV_m2) (s s' : 'cV_P) (t : 'cV_Q),
 S0 s -> S0 s' -> T t -> `|Y z s t - Y z s' t| <= c * frobenius z * frobenius (s - s')) ->
(forall (z : 'rV_m2) (s : 'cV_P) (t t' : 'cV_Q),
 S0 s -> T t -> T t' -> `|Y z s t - Y z s t'| <= c * frobenius z * frobenius (t - t')) ->
(forall (w w' : 'rV_m1) (s : 'cV_P) (t : 'cV_Q),
 S0 s -> T t -> `|X w s t - X w' s t| <= c * frobenius (w - w')) ->
(forall (z z' : 'rV_m2) (s : 'cV_P) (t : 'cV_Q),
 S0 s -> T t -> `|Y z s t - Y z' s t| <= c * frobenius (z - z')) ->
(forall (k l : nat) (rs : 'I_k.+1 -> 'cV_P) (cs : 'I_l.+1 -> 'cV_Q),
 (forall u : 'I_k.+1, S0 (rs u)) ->
 (forall t : 'I_l.+1, T (cs t)) ->
 (\int[gauss m2]_z (minmax (\matrix_(u, t) Y z (rs u) (cs t)))%:E <=
  \int[gauss m1]_w (minmax (\matrix_(u, t) X w (rs u) (cs t)))%:E)%E) ->
\int[gauss m2]_z infsup S0 T (Y z) <= \int[gauss m1]_w infsup S0 T (X w)

Gordon's comparison for bounded index sets.

Main result

Stated in the README together with gordon_gamma.

Statement as written in the source

Theorem infsup_compare :
  \int[gauss m2]_z infsup S T (Y z) <= \int[gauss m1]_w infsup S T (X w).

Used by 2 declarations in 1 file

this file: cgmt_lower, cgmt_upper

sectionblock_norms

Context {R : realType}.

lemma frobenius_hsub_sqr source, line 522

forall {R : realType} [m n1 n2 : nat] (w : 'M_(m, n1 + n2)),
frobenius w ^+ 2 = frobenius (lsubmx w) ^+ 2 + frobenius (rsubmx w) ^+ 2

Statement as written in the source

Lemma frobenius_hsub_sqr m n1 n2 (w : 'M[R]_(m, n1 + n2)) :
  frobenius w ^+ 2 = frobenius (lsubmx w) ^+ 2 + frobenius (rsubmx w) ^+ 2.

Used by 3 declarations in 1 file

this file: frobenius_lsubmx_le, frobenius_rsubmx_le, frobenius_hsub_add

lemma frobenius_lsubmx_le source, line 529

forall {R : realType} [m n1 n2 : nat] (w : 'M_(m, n1 + n2)),
frobenius (lsubmx w) <= frobenius w

Statement as written in the source

Lemma frobenius_lsubmx_le m n1 n2 (w : 'M[R]_(m, n1 + n2)) :
  frobenius (lsubmx w) <= frobenius w.

Used by 4 declarations in 1 file

this file: nA, dotg, cgmt_lower, cgmt_upper

lemma frobenius_rsubmx_le source, line 536

forall {R : realType} [m n1 n2 : nat] (w : 'M_(m, n1 + n2)),
frobenius (rsubmx w) <= frobenius w

Statement as written in the source

Lemma frobenius_rsubmx_le m n1 n2 (w : 'M[R]_(m, n1 + n2)) :
  frobenius (rsubmx w) <= frobenius w.

Used by 4 declarations in 1 file

this file: ng, doth, cgmt_lower, cgmt_upper

lemma frobenius_hsub_add source, line 543

forall {R : realType} [m n1 n2 : nat] (w : 'M_(m, n1 + n2)),
frobenius (lsubmx w) + frobenius (rsubmx w) <= Num.ExtraDef.sqrtr 2 * frobenius w

Statement as written in the source

Lemma frobenius_hsub_add m n1 n2 (w : 'M[R]_(m, n1 + n2)) :
  frobenius (lsubmx w) + frobenius (rsubmx w) <= Num.sqrt 2 * frobenius w.

Used by 2 declarations in 2 files

this file: cgmt_aux_lipschitz
GaussianAnalysis.comparison.cone_escape: F_lip

lemma mxdot_mulmx_le source, line 553

forall {R : realType} [n m : nat] (A : 'M_(n, m)) (x : 'cV_m) (y : 'cV_n),
`|mxdot y (A *m x)| <= frobenius y * (frobenius A * frobenius x)

Statement as written in the source

Lemma mxdot_mulmx_le n m (A : 'M[R]_(n, m)) (x : 'cV[R]_m) (y : 'cV[R]_n) :
  `|mxdot y (A *m x)| <= frobenius y * (frobenius A * frobenius x).

Used by 6 declarations in 1 file

this file: escape_inf_minimax, Xp_b, Xp_x, Xp_y, Xp_w, up_X

lemma unit_dir source, line 561

forall {R : realType} [n : nat] (g : 'rV_n),
(0 < n)%N -> exists y : 'cV_n, frobenius y = 1 /\ mxdot g^T y = frobenius g

A unit vector of 'cV[R]_n on which <g, y> = |g|.

Statement as written in the source

Lemma unit_dir n (g : 'rV[R]_n) : (0 < n)%N ->
  exists y : 'cV[R]_n, frobenius y = 1 /\ mxdot g^T y = frobenius g.

Used by 1 declaration in 1 file

this file: low_aux

lemma max0_leD source, line 577

forall {R : realType} [a b c : R], 0 <= c -> a <= b + c -> maxr 0 a <= maxr 0 b + c

max (0, a) <= max (0, b) + c when a <= b + c and c >= 0.

Statement as written in the source

Lemma max0_leD (a b c : R) : 0 <= c -> a <= b + c ->
  Num.max 0 a <= Num.max 0 b + c.

Used by 2 declarations in 2 files

this file: cgmt_aux_lipschitz
GaussianAnalysis.comparison.cone_escape: F0_lip

sectioncgmt_aux

Context {R : realType} {N M : nat}.
Variable K : set 'cV[R]_M.
Hypothesis K0 : K !=set0.

definition cgmt_aux main result source, line 593

Type

forall {R : realType} {N M : nat}, set 'cV_M -> 'rV_N -> 'rV_M -> R

Definition

Definition cgmt_aux (g : 'rV[R]_N) (h : 'rV[R]_M) : R :=
  inf [set Num.max 0 (frobenius g * frobenius x - mxdot h^T x) | x in K].

phi(K) at g and h: inf_(x in K) (|g| |x| - <h, x>)_+.

Main result

Stated in the README together with cgmt_lower.

Used by 22 declarations in 2 files

this file: cgmt_aux_le, cgmt_aux_ge, cgmt_aux_ge0, cgmt_auxNl, cgmt_aux_lipschitz, low_aux, cgmt_lower, up_Y, cgmt_upper, cgmt_aux_tail, cgmt_tail, measurable_cgmt_aux, cgmt_aux_tr_set, cgmt_aux_mean_zero, cgmt_zero_tail
GaussianAnalysis.comparison.cone_escape: cgmt_aux_cone_zero, cgmt_aux_cone_zero_lt, cgmt_aux_cone_ge, cgmt_aux_tr_cone_zero, cgmt_aux_tr_cone_ge, mphi, cone_escape_lower_tail

lemma cgmt_aux_le source, line 596

forall {R : realType} {N M : nat} [K : set 'cV_M] (g : 'rV_N) (h : 'rV_M) [x : 'cV_M],
K x -> cgmt_aux K g h <= maxr 0 (frobenius g * frobenius x - mxdot h^T x)

Statement as written in the source

Lemma cgmt_aux_le g h x : K x ->
  cgmt_aux g h <= Num.max 0 (frobenius g * frobenius x - mxdot h^T x).

Used by 3 declarations in 2 files

this file: cgmt_aux_lipschitz, low_aux
GaussianAnalysis.comparison.cone_escape: cgmt_aux_cone_zero

lemma cgmt_aux_ge source, line 603

forall {R : realType} {N M : nat} [K : set 'cV_M],
K !=set0 ->
forall [g : 'rV_N] [h : 'rV_M]
  [c : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R],
(forall x : 'cV_M, K x -> c <= maxr 0 (frobenius g * frobenius x - mxdot h^T x)) ->
c <= cgmt_aux K g h

Statement as written in the source

Lemma cgmt_aux_ge g h c :
  (forall x, K x -> c <= Num.max 0 (frobenius g * frobenius x - mxdot h^T x)) ->
  c <= cgmt_aux g h.

Used by 4 declarations in 2 files

this file: cgmt_aux_ge0, cgmt_aux_lipschitz, up_Y
GaussianAnalysis.comparison.cone_escape: cgmt_aux_cone_ge

lemma cgmt_aux_ge0 source, line 613

forall {R : realType} {N M : nat} [K : set 'cV_M],
K !=set0 -> forall (g : 'rV_N) (h : 'rV_M), 0 <= cgmt_aux K g h

Statement as written in the source

Lemma cgmt_aux_ge0 g h : 0 <= cgmt_aux g h.

Used by 2 declarations in 2 files

this file: cgmt_aux_mean_zero
GaussianAnalysis.comparison.cone_escape: cgmt_aux_cone_zero

lemma cgmt_auxNl source, line 617

forall {R : realType} {N M : nat} (K : set 'cV_M)
  (g : 'rV[R]_N) (h : 'rV_M),
cgmt_aux K (- g) h = cgmt_aux K g h

phi(K) does not change when (g, h) is replaced by (- g, h).

Statement as written in the source

Lemma cgmt_auxNl g h : cgmt_aux (- g) h = cgmt_aux g h.

Variable rho : R.
Hypothesis Kb : forall x, K x -> frobenius x <= rho.

lemma cgmt_aux_lipschitz source, line 623

forall {R : realType} {N M : nat} [K : set 'cV_M],
K !=set0 ->
forall [rho : R],
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
forall z z' : 'rV_(N + M),
`|cgmt_aux K (lsubmx z) (rsubmx z) - cgmt_aux K (lsubmx z') (rsubmx z')| <=
Num.ExtraDef.sqrtr 2 * rho * frobenius (z - z')

Statement as written in the source

Lemma cgmt_aux_lipschitz (z z' : 'rV[R]_(N + M)) :
  `|cgmt_aux (lsubmx z) (rsubmx z) - cgmt_aux (lsubmx z') (rsubmx z')| <=
  Num.sqrt 2 * rho * frobenius (z - z').

Used by 5 declarations in 2 files

this file: cgmt_lower, cgmt_upper, cgmt_aux_tail, measurable_cgmt_aux
GaussianAnalysis.comparison.cone_escape: cone_escape_lower_tail

sectioncV_compact

Context {R : realType}.

lemma mx_norm_frobenius source, line 666

forall {R : realType} [m n : nat] (B : 'M_(m, n)), `|B| <= frobenius B

Statement as written in the source

Lemma mx_norm_frobenius m n (B : 'M[R]_(m, n)) : `|B| <= frobenius B.

Used by 1 declaration in 1 file

this file: closed_bounded_compact_cV

lemma continuous_trmx source, line 673

forall {R : realType} [m n : nat], continuous [eta trmx]

Statement as written in the source

Lemma continuous_trmx m n : continuous (fun B : 'M[R]_(m, n) => B^T).

Used by 3 declarations in 2 files

this file: closed_bounded_compact_cV, closed_tr_set
GaussianAnalysis.comparison.cone_escape: cone_sup_attained

lemma closed_bounded_compact_cV main result source, line 686

forall {R : realType} [n : nat] [A : set 'cV_n] [r : R],
closed A -> (forall x : 'cV_n, A x -> frobenius x <= r) -> compact A

A closed and bounded set of column vectors is compact.

Main result

Stated in the README together with gordon_gamma.

Statement as written in the source

Lemma closed_bounded_compact_cV n (A : set 'cV[R]_n) (r : R) :
  closed A -> (forall x, A x -> frobenius x <= r) -> compact A.

Used by 2 declarations in 2 files

this file: escape_inf_minimax
GaussianAnalysis.comparison.cone_escape: cone_sup_attained

sectionminimax

Context {R : realType} {N M : nat}.
Variables (K : set 'cV[R]_M) (rho : R).
Hypotheses (K0 : K !=set0) (Kb : forall x, K x -> frobenius x <= rho).

lemma continuous_frobenius_mulmx source, line 710

forall {R : realType} {N M : nat} [A : 'M_(N, M)],
continuous (fun x0 : 'cV_M => frobenius (A *m x0))

Statement as written in the source

Lemma continuous_frobenius_mulmx (A : 'M[R]_(N, M)) :
  continuous (fun x : 'cV[R]_M => frobenius (A *m x)).

Used by 2 declarations in 2 files

this file: escape_inf_minimax
GaussianAnalysis.comparison.cone_escape: cone_sup_attained

lemma escape_inf_lip source, line 729

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
forall A A' : 'M_(N, M), `|escape_inf K A - escape_inf K A'| <= rho * frobenius (A - A')

inf_(x in K) |A x| is rho-Lipschitz in A.

Statement as written in the source

Lemma escape_inf_lip (A A' : 'M[R]_(N, M)) :
  `|escape_inf K A - escape_inf K A'| <= rho * frobenius (A - A').

Used by 5 declarations in 1 file

this file: cgmt_lower, cgmt_upper, cgmt_escape_tail, cgmt_tail, measurable_escape_inf

Hypothesis Kc : closed K.
Hypothesis Kcvx : forall x y (t : R), K x -> K y -> 0 <= t <= 1 ->
  K (x + t *: (y - x)).

lemma escape_inf_minimax main result source, line 752

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
closed K ->
(forall (x y : 'cV_M) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
forall A : 'M_(N, M),
escape_inf K A <=
- infsup (unit_ball (n:=N)) K (fun (y : 'cV_N) (x : 'cV_M) => mxdot y (A *m x))

The minimax exchange: for K convex and compact, inf_(x in K) |A x| <= sup_(|y| <= 1) inf_(x in K) <y, A x>, written as - inf_(|y| <= 1) sup_(x in K) <y, A x> since the unit ball is symmetric. The y is the direction of the point of A K nearest to 0.

Main result

Stated in the README together with gordon_gamma.

Statement as written in the source

Lemma escape_inf_minimax (A : 'M[R]_(N, M)) :
  escape_inf K A <= - infsup (@unit_ball R N) K (fun y x => mxdot y (A *m x)).

Used by 1 declaration in 1 file

this file: up_X

sectioncgmt_mean

Context {R : realType} {N M : nat}.
Variables (K : set 'cV[R]_M) (rho : R).
Hypotheses (K0 : K !=set0) (Kb : forall x, K x -> frobenius x <= rho).
Local Notation B := (@unit_ball R N).

let rho0 section-local source, line 814

Let rho0 : 0 <= rho.

Used by 10 declarations in 1 file

this file: c0, Xp_b, Xp_x, Xp_w, Yp_b, Yp_x, Yp_z, cgmt_lower, up_X, cgmt_upper

let B0 section-local source, line 817

Let B0 : B !=set0.

Used by 5 declarations in 1 file

this file: low_X, cgmt_lower, up_X, up_Y, cgmt_upper

let Bb section-local source, line 820

Let Bb y : B y -> frobenius y <= 1.

Used by 11 declarations in 1 file

this file: Xp_b, Xp_x, Xp_w, Yp_b, Yp_x, Yp_z, low_X, cgmt_lower, up_X, up_Y, cgmt_upper

let Xp section-local source, line 824

Let Xp (w : 'rV[R]_(N * M + 1)) (x : 'cV[R]_M) (y : 'cV[R]_N) : R :=
  mxdot y ((vec_mx (lsubmx w) : 'M[R]_(N, M)) *m x) +
  rsubmx w 0 0 * (frobenius x * frobenius y).

y^T A x + gamma |x| |y|, for w = (a, gamma) and A = vec_mx a.

Used by 10 declarations in 1 file

this file: Xp_b, Xp_x, Xp_y, Xp_w, XY_low, XY_up, low_X, cgmt_lower, up_X, cgmt_upper

let Yp section-local source, line 829

Let Yp (z : 'rV[R]_(N + M)) (x : 'cV[R]_M) (y : 'cV[R]_N) : R :=
  frobenius x * mxdot (lsubmx z)^T y + frobenius y * mxdot (rsubmx z)^T x.

|x| <g, y> + |y| <h, x>, for z = (g, h).

Used by 10 declarations in 1 file

this file: Yp_b, Yp_x, Yp_y, Yp_z, XY_low, XY_up, low_aux, cgmt_lower, up_Y, cgmt_upper

let c section-local source, line 832

Let c := 2 * (rho + 1).

Used by 12 declarations in 1 file

this file: c0, Xp_b, Xp_x, Xp_y, Xp_w, Yp_b, Yp_x, Yp_y, Yp_z, up_X, up_Y, cgmt_upper

let c0 section-local source, line 834

Let c0 : 0 <= c.

Used by 2 declarations in 1 file

this file: cgmt_lower, cgmt_upper

let le3 section-local source, line 838

Let le3 (a b d a' b' d' : R) : 0 <= a -> 0 <= b -> 0 <= d ->
  a <= a' -> b <= b' -> d <= d' -> a * (b * d) <= a' * (b' * d').

Used by 5 declarations in 1 file

this file: Xp_b, Xp_x, Xp_y, Xp_w, up_X

let nA section-local source, line 845

Let nA (w : 'rV[R]_(N * M + 1)) :
  frobenius (vec_mx (lsubmx w) : 'M[R]_(N, M)) <= frobenius w.

Used by 5 declarations in 1 file

this file: Xp_b, Xp_x, Xp_y, Xp_w, up_X

let ng section-local source, line 849

Let ng (w : 'rV[R]_(N * M + 1)) : `|rsubmx w 0 0| <= frobenius w.

Used by 4 declarations in 1 file

this file: Xp_b, Xp_x, Xp_y, Xp_w

let dotg section-local source, line 852

Let dotg (z : 'rV[R]_(N + M)) (y : 'cV[R]_N) :
  `|mxdot (lsubmx z)^T y| <= frobenius z * frobenius y.

Used by 4 declarations in 1 file

this file: Yp_b, Yp_x, Yp_y, Yp_z

let doth section-local source, line 859

Let doth (z : 'rV[R]_(N + M)) (x : 'cV[R]_M) :
  `|mxdot (rsubmx z)^T x| <= frobenius z * frobenius x.

Used by 4 declarations in 1 file

this file: Yp_b, Yp_x, Yp_y, Yp_z

let Xp_b section-local source, line 866

Let Xp_b w x y : K x -> B y -> `|Xp w x y| <= c * frobenius w.

Used by 4 declarations in 1 file

this file: low_X, cgmt_lower, up_X, cgmt_upper

let Xp_x section-local source, line 884

Let Xp_x w x x' y : K x -> K x' -> B y ->
  `|Xp w x y - Xp w x' y| <= c * frobenius w * frobenius (x - x').

Used by 2 declarations in 1 file

this file: cgmt_lower, cgmt_upper

let Xp_y section-local source, line 909

Let Xp_y w x y y' : K x -> B y -> B y' ->
  `|Xp w x y - Xp w x y'| <= c * frobenius w * frobenius (y - y').

Used by 2 declarations in 1 file

this file: cgmt_lower, cgmt_upper

let Xp_w section-local source, line 934

Let Xp_w w w' x y : K x -> B y ->
  `|Xp w x y - Xp w' x y| <= c * frobenius (w - w').

Used by 2 declarations in 1 file

this file: cgmt_lower, cgmt_upper

let Yp_b section-local source, line 958

Let Yp_b z x y : K x -> B y -> `|Yp z x y| <= c * frobenius z.

Used by 4 declarations in 1 file

this file: low_aux, cgmt_lower, up_Y, cgmt_upper

let Yp_x section-local source, line 976

Let Yp_x z x x' y : K x -> K x' -> B y ->
  `|Yp z x y - Yp z x' y| <= c * frobenius z * frobenius (x - x').

Used by 2 declarations in 1 file

this file: cgmt_lower, cgmt_upper

let Yp_y section-local source, line 1000

Let Yp_y z x y y' : K x -> B y -> B y' ->
  `|Yp z x y - Yp z x y'| <= c * frobenius z * frobenius (y - y').

Used by 2 declarations in 1 file

this file: cgmt_lower, cgmt_upper

let Yp_z section-local source, line 1024

Let Yp_z z z' x y : K x -> B y ->
  `|Yp z x y - Yp z' x y| <= c * frobenius (z - z').

Used by 2 declarations in 1 file

this file: cgmt_lower, cgmt_upper

let XY_low section-local source, line 1050

Let XY_low k l (rs : 'I_k.+1 -> 'cV[R]_M) (cs : 'I_l.+1 -> 'cV[R]_N) :
  (forall u, K (rs u)) -> (forall t, B (cs t)) ->
  (\int[gauss (N + M)]_z (minmax (\matrix_(u, t) Yp z (rs u) (cs t)))%:E <=
   \int[gauss (N * M + 1)]_w (minmax (\matrix_(u, t) Xp w (rs u) (cs t)))%:E)%E.

The finite comparisons, from gordon_gamma.

Used by 1 declaration in 1 file

this file: cgmt_lower

let XY_up section-local source, line 1070

Let XY_up k l (rs : 'I_k.+1 -> 'cV[R]_N) (cs : 'I_l.+1 -> 'cV[R]_M) :
  (forall u, B (rs u)) -> (forall t, K (cs t)) ->
  (\int[gauss (N + M)]_z (minmax (\matrix_(u, t) Yp z (cs t) (rs u)))%:E <=
   \int[gauss (N * M + 1)]_w (minmax (\matrix_(u, t) Xp w (cs t) (rs u)))%:E)%E.

Used by 1 declaration in 1 file

this file: cgmt_upper

let low_aux section-local source, line 1088

Let low_aux z : (0 < N)%N ->
  cgmt_aux K (lsubmx (- z)) (rsubmx (- z)) <= infsup K B (Yp z).

The pointwise bounds of the lower bound.

Used by 1 declaration in 1 file

this file: cgmt_lower

let low_X section-local source, line 1103

Let low_X w : infsup K B (Xp w) <=
  escape_inf K (vec_mx (lsubmx w) : 'M[R]_(N, M)) +
  rho * frobenius (rsubmx w).

Used by 1 declaration in 1 file

this file: cgmt_lower

theorem cgmt_lower main result source, line 1126

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
(0 < N)%N ->
\int[gauss (N + M)]_z cgmt_aux K (lsubmx z) (rsubmx z) - rho <=
\int[gauss (N * M)]_a escape_inf K (vec_mx a : 'M_(N, M))

The lower bound of the convex Gaussian min-max theorem.

Main result, as the README states it

The convex Gaussian min-max theorem in mean form (Theorem 5.3 of Koehler and Sohn; Thrampoulidis, Oymak and Hassibi, Theorem 3): let A = vec_mx a be an N x M matrix of independent standard normal entries, z = (g, h) of law gauss (N + M), and K a nonempty set of 'cV[R]_M with |x| <= rho on K; let Phi(K) = inf_(x in K) |A x| (escape_inf) and phi(K) = inf_(x in K) (|g| |x| - <h, x>)_+ (cgmt_aux). Then E Phi(K) >= E phi(K) - rho for N > 0, and E Phi(K) <= E phi(K) + rho for K closed and convex.

Statement as written in the source

Theorem cgmt_lower : (0 < N)%N ->
  \int[gauss (N + M)]_z cgmt_aux K (lsubmx z) (rsubmx z) - rho <=
  \int[gauss (N * M)]_a escape_inf K (vec_mx a : 'M[R]_(N, M)).

Used by 2 declarations in 2 files

this file: cgmt_tail
GaussianAnalysis.comparison.cone_escape: cone_escape_lower_tail

sectionupper

Hypothesis Kc : closed K.
Hypothesis Kcvx : forall x y (t : R), K x -> K y -> 0 <= t <= 1 ->
  K (x + t *: (y - x)).

let up_X section-local source, line 1202

Let up_X w : escape_inf K (vec_mx (lsubmx w) : 'M[R]_(N, M)) +
  infsup B K (fun y x => Xp w x y) <= rho * frobenius (rsubmx w).

The pointwise bounds of the upper bound.

Used by 1 declaration in 1 file

this file: cgmt_upper

let up_Y section-local source, line 1232

Let up_Y z :
  0 <= cgmt_aux K (lsubmx z) (rsubmx z) + infsup B K (fun y x => Yp z x y).

Used by 1 declaration in 1 file

this file: cgmt_upper

theorem cgmt_upper main result source, line 1257

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
closed K ->
(forall (x y : 'cV_M) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
\int[gauss (N * M)]_a escape_inf K (vec_mx a : 'M_(N, M)) <=
\int[gauss (N + M)]_z cgmt_aux K (lsubmx z) (rsubmx z) + rho

The upper bound of the convex Gaussian min-max theorem, for K convex.

Main result

Stated in the README together with cgmt_lower.

Statement as written in the source

Theorem cgmt_upper :
  \int[gauss (N * M)]_a escape_inf K (vec_mx a : 'M[R]_(N, M)) <=
  \int[gauss (N + M)]_z cgmt_aux K (lsubmx z) (rsubmx z) + rho.

Used by 1 declaration in 1 file

this file: cgmt_tail

theorem cgmt_escape_tail main result source, line 1348

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
forall [u : R],
0 <= u ->
(gauss (N * M)
   [set a | (u <=
             `|escape_inf K (vec_mx a : 'M_(N, M)) -
               \int[gauss (N * M)]_b escape_inf K (vec_mx b : 'M_(N, M))|)%R] <=
 (2 * expR (- u ^+ 2 / (2 * rho ^+ 2)))%:E)%E

Concentration: Phi(K) is rho-Lipschitz in a, and phi(K) is (sqrt 2 rho)-Lipschitz in z.

Main result, as the README states it

Phi(K) is rho-Lipschitz in a and phi(K) is sqrt 2 rho-Lipschitz in z, so they are at least u away from their means with probability at most 2 exp (- u^2 / (2 rho^2)) and 2 exp (- u^2 / (4 rho^2)). For N > 0 and K closed and convex, Phi(K) is at least rho + u away from E phi(K) with probability at most 2 exp (- u^2 / (2 rho^2)).

Statement as written in the source

Theorem cgmt_escape_tail (u : R) : 0 <= u ->
  (gauss (N * M) [set a | u <= `|escape_inf K (vec_mx a : 'M[R]_(N, M)) -
     \int[gauss (N * M)]_b escape_inf K (vec_mx b : 'M[R]_(N, M))|]%R <=
   (2 * expR (- u ^+ 2 / (2 * rho ^+ 2)))%:E)%E.

Used by 2 declarations in 2 files

this file: cgmt_tail
GaussianAnalysis.comparison.cone_escape: cone_escape_lower_tail

theorem cgmt_aux_tail main result source, line 1362

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
forall [u : R],
0 <= u ->
(gauss (N + M)
   [set z | (u <=
             `|cgmt_aux K (lsubmx z) (rsubmx z) -
               \int[gauss (N + M)]_y cgmt_aux K (lsubmx y) (rsubmx y)|)%R] <=
 (2 * expR (- u ^+ 2 / (4 * rho ^+ 2)))%:E)%E

Main result

Stated in the README together with cgmt_escape_tail.

Statement as written in the source

Theorem cgmt_aux_tail (u : R) : 0 <= u ->
  (gauss (N + M) [set z | u <= `|cgmt_aux K (lsubmx z) (rsubmx z) -
     \int[gauss (N + M)]_y cgmt_aux K (lsubmx y) (rsubmx y)|]%R <=
   (2 * expR (- u ^+ 2 / (4 * rho ^+ 2)))%:E)%E.

Used by 1 declaration in 1 file

this file: cgmt_aux_mean_zero

corollary cgmt_tail main result source, line 1376

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
forall [u : R],
(0 < N)%N ->
closed K ->
(forall (x y : 'cV_M) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
0 <= u ->
(gauss (N * M)
   [set a | (rho + u <=
             `|escape_inf K (vec_mx a : 'M_(N, M)) -
               \int[gauss (N + M)]_z cgmt_aux K (lsubmx z) (rsubmx z)|)%R] <=
 (2 * expR (- u ^+ 2 / (2 * rho ^+ 2)))%:E)%E

Phi(K) concentrates around the mean of phi(K): for K closed and convex and N > 0, Phi(K) is farther than rho + u from E phi(K) with probability at most 2 exp (- u^2 / (2 rho^2)).

Main result

Stated in the README together with cgmt_escape_tail.

Statement as written in the source

Corollary cgmt_tail (u : R) : (0 < N)%N -> closed K ->
  (forall x y (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
  0 <= u ->
  (gauss (N * M) [set a | rho + u <= `|escape_inf K (vec_mx a : 'M[R]_(N, M)) -
     \int[gauss (N + M)]_z cgmt_aux K (lsubmx z) (rsubmx z)|]%R <=
   (2 * expR (- u ^+ 2 / (2 * rho ^+ 2)))%:E)%E.

Used by 1 declaration in 1 file

this file: cgmt_zero_tail

sectioncgmt_laws

Context {R : realType} {N M : nat}.
Variables (K : set 'cV[R]_M) (rho : R).
Hypotheses (K0 : K !=set0) (Kb : forall x, K x -> frobenius x <= rho).

lemma measurable_escape_inf main result source, line 1422

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
measurable_fun [set: 'rV_(N * M)]
  (fun a : 'rV_(N * M) => escape_inf K (vec_mx a : 'M_(N, M)))

Phi and phi are Lipschitz, hence measurable, functions of the Gaussian entries, so that their laws are defined.

Main result, as the README states it

Phi(K) and phi(K) are measurable functions of the Gaussian entries, so that their laws are defined. For a set K of row vectors, the theorems apply to the set tr_set K of the transposes, with Phi = inf_(x in K) |A x^T| and phi = inf_(x in K) (|g| |x| - <h, x>)_+; tr_set K is nonempty, bounded, closed or convex with K.

Statement as written in the source

Lemma measurable_escape_inf : measurable_fun setT
  (fun a : 'rV[R]_(N * M) => escape_inf K (vec_mx a : 'M[R]_(N, M))).

Used by 2 declarations in 2 files

this file: cgmt_zero_tail
GaussianAnalysis.comparison.cone_escape: mPhi

lemma measurable_cgmt_aux main result source, line 1430

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
measurable_fun [set: 'rV_(N + M)]
  (fun z : 'rV_(N + M) => cgmt_aux K (lsubmx z) (rsubmx z))

Main result

Stated in the README together with measurable_escape_inf.

Statement as written in the source

Lemma measurable_cgmt_aux : measurable_fun setT
  (fun z : 'rV[R]_(N + M) => cgmt_aux K (lsubmx z) (rsubmx z)).

Used by 2 declarations in 2 files

this file: cgmt_aux_mean_zero
GaussianAnalysis.comparison.cone_escape: mphi

sectioncgmt_rows

Context {R : realType} {M : nat}.
Variable K : set 'rV[R]_M.

definition tr_set main result source, line 1447

Type

forall {R : realType} {M : nat}, set 'rV_M -> set 'cV_M

Definition

Definition tr_set : set 'cV[R]_M := [set x^T | x in K].

The theorems above take a set of column vectors; for a set K of row vectors they apply to the set tr_set K of the transposes, and the following lemmas write Phi, phi and the hypotheses in terms of K.

Main result

Stated in the README together with measurable_escape_inf.

Used by 16 declarations in 2 files

this file: tr_setE, escape_inf_tr_set, cgmt_aux_tr_set, tr_set_neq0, tr_set_bounded, closed_tr_set, convex_tr_set
GaussianAnalysis.comparison.cone_escape: cone_sup_tr_setE, cone_sup_proj, tr_set0, tr_set_cone, tr_set_base, tr_set_sub, tr_set_norm_ge, cgmt_aux_tr_cone_zero, cgmt_aux_tr_cone_ge

lemma tr_setE source, line 1449

forall {R : realType} {M : nat} (K : set 'rV_M), tr_set K = [set y | K y^T]

Statement as written in the source

Lemma tr_setE : tr_set = [set y | K y^T].

Used by 1 declaration in 1 file

this file: closed_tr_set

lemma escape_inf_tr_set main result source, line 1455

forall {R : realType} {M : nat} (K : set 'rV_M) [N : nat] (A : 'M_(N, M)),
escape_inf (tr_set K) A = inf [set frobenius (A *m x^T) | x in K]

Main result

Stated in the README together with measurable_escape_inf.

Statement as written in the source

Lemma escape_inf_tr_set N (A : 'M[R]_(N, M)) :
  escape_inf tr_set A = inf [set frobenius (A *m x^T) | x in K].

lemma cgmt_aux_tr_set main result source, line 1463

forall {R : realType} {M : nat} (K : set 'rV_M) [N : nat] (g : 'rV_N) (h : 'rV_M),
cgmt_aux (tr_set K) g h = inf [set maxr 0 (frobenius g * frobenius x - mxdot h x) | x in K]

Main result

Stated in the README together with measurable_escape_inf.

Statement as written in the source

Lemma cgmt_aux_tr_set N (g : 'rV[R]_N) (h : 'rV[R]_M) :
  cgmt_aux tr_set g h =
  inf [set Num.max 0 (frobenius g * frobenius x - mxdot h x) | x in K].

lemma tr_set_neq0 source, line 1474

forall {R : realType} {M : nat} [K : set 'rV_M], K !=set0 -> tr_set K !=set0

Statement as written in the source

Lemma tr_set_neq0 : K !=set0 -> tr_set !=set0.

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.cone_escape: cgmt_aux_tr_cone_ge

lemma tr_set_bounded source, line 1477

forall {R : realType} {M : nat} [K : set 'rV_M] [rho : R],
(forall x : 'rV_M, K x -> frobenius x <= rho) ->
forall [y : 'cV_M], tr_set K y -> frobenius y <= rho

Statement as written in the source

Lemma tr_set_bounded (rho : R) : (forall x, K x -> frobenius x <= rho) ->
  forall y, tr_set y -> frobenius y <= rho.

lemma closed_tr_set source, line 1481

forall {R : realType} {M : nat} [K : set 'rV_M], closed K -> closed (tr_set K)

Statement as written in the source

Lemma closed_tr_set : closed K -> closed tr_set.

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.cone_escape: cgmt_aux_tr_cone_zero

lemma convex_tr_set source, line 1487

forall {R : realType} {M : nat} [K : set 'rV_M],
(forall (x y : 'rV_M) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
forall [x y : 'cV_M] [t : R],
tr_set K x -> tr_set K y -> 0 <= t <= 1 -> tr_set K (x + t *: (y - x))

Statement as written in the source

Lemma convex_tr_set : (forall x y (t : R), K x -> K y -> 0 <= t <= 1 ->
    K (x + t *: (y - x))) ->
  forall x y (t : R), tr_set x -> tr_set y -> 0 <= t <= 1 ->
    tr_set (x + t *: (y - x)).

sectioncgmt_zero

Context {R : realType} {N M : nat}.
Variables (K : set 'cV[R]_M) (rho : R).
Hypotheses (K0 : K !=set0) (Kb : forall x, K x -> frobenius x <= rho).
Local Open Scope ereal_scope.

lemma cgmt_aux_mean_zero main result source, line 1507

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
0 < rho ->
((2^-1)%:E < gauss (N + M) [set z | cgmt_aux K (lsubmx z) (rsubmx z) = 0%R])%E ->
\int[gauss (N + M)]_z cgmt_aux K (lsubmx z) (rsubmx z) <=
2 * rho * Num.ExtraDef.sqrtr (ln 4)

If phi(K) vanishes with probability more than 1/2, its mean is at most 2 rho sqrt (ln 4), by its concentration.

Main result, as the README states it

If phi(K) vanishes with probability more than 1/2, then E phi(K) <= 2 rho sqrt (ln 4) (concentration), and Phi(K) >= rho (1 + 2 sqrt (ln 4)) + u has probability at most 2 exp (- u^2 / (2 rho^2)): the approximate solutions of A x = 0 on K that the CGMT gives when the auxiliary problem has the value 0.

Statement as written in the source

Lemma cgmt_aux_mean_zero : (0 < rho)%R ->
  (2^-1)%:E <
    gauss (N + M) [set z | cgmt_aux K (lsubmx z) (rsubmx z) = 0%R] ->
  (\int[gauss (N + M)]_z cgmt_aux K (lsubmx z) (rsubmx z) <=
   2 * rho * Num.sqrt (ln 4))%R.

Used by 1 declaration in 1 file

this file: cgmt_zero_tail

theorem cgmt_zero_tail main result source, line 1554

forall {R : realType} {N M : nat} [K : set 'cV_M] [rho : R],
K !=set0 ->
(forall x : 'cV_M, K x -> frobenius x <= rho) ->
forall [u : R],
(0 < N)%N ->
0 < rho ->
closed K ->
(forall (x y : 'cV_M) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
0 <= u ->
((2^-1)%:E < gauss (N + M) [set z | cgmt_aux K (lsubmx z) (rsubmx z) = 0%R])%E ->
(gauss (N * M)
   [set a | (rho * (1 + 2 * Num.ExtraDef.sqrtr (ln 4)) + u <=
             escape_inf K (vec_mx a : 'M_(N, M)))%R] <=
 (2 * expR (- u ^+ 2 / (2 * rho ^+ 2)))%:E)%E

Then Phi(K) exceeds rho (1 + 2 sqrt (ln 4)) + u with probability at most 2 exp (- u^2 / (2 rho^2)): the approximate solutions that the CGMT gives when the auxiliary problem has the value 0.

Main result

Stated in the README together with cgmt_aux_mean_zero.

Statement as written in the source

Theorem cgmt_zero_tail (u : R) : (0 < N)%N -> (0 < rho)%R -> closed K ->
  (forall x y (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x)))%R ->
  (0 <= u)%R ->
  (2^-1)%:E <
    gauss (N + M) [set z | cgmt_aux K (lsubmx z) (rsubmx z) = 0%R] ->
  gauss (N * M) [set a | rho * (1 + 2 * Num.sqrt (ln 4)) + u <=
     escape_inf K (vec_mx a : 'M[R]_(N, M))]%R <=
  (2 * expR (- u ^+ 2 / (2 * rho ^+ 2)))%:E.

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.cone_escape: cone_escape_zero_tail

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.