GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysiscomparisoncone_escape

The convex Gaussian min-max theorem on cones

GaussianAnalysis.comparison.cone_escapelibrary/comparison/cone_escape.v458 lines21 lemmas and theorems, 1 definitionsource
Imports 9 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

Required by 5 files of the paper proofs

Vectors x of R^M are column vectors 'cV[R]_M and h : 'rV[R]_M, as in cgmt.v; |x| is frobenius x and <h, x> is mxdot h^T x. Let K be a set of 'cV[R]_M that contains 0 and

sigma_K(h) = sup_(x in K, |x| <= 1) <h, x>              (cone_sup K h).

Let B be a set of 'cV[R]_M such that every nonzero point of K has a positive multiple in B (a base of K when B is in K and 0 is not in B). The auxiliary value of the CGMT on B (cgmt.v),

phi(B) = cgmt_aux B g h = inf_(x in B) (|g| |x| - <h, x>)_+,

is governed by the sign of |g| - sigma_K(h):

  • cgmt_aux_cone_zero: for K closed, phi(B) = 0 when 0 < sigma_K(h) and |g| <= sigma_K(h), in particular when 0 < |g| <= sigma_K(h) or |g| < sigma_K(h) (cgmt_aux_cone_zero_lt): at a point x of K with |x| <= 1 and <h, x> = sigma_K(h), the multiples a x with a > 0 have |g| |a x| - <h, a x> <= 0;
  • cgmt_aux_cone_ge: for a cone K, B nonempty and in K, and r <= |x| on B, phi(B) >= r (|g| - sigma_K(h))_+, since <h, x> <= |x| sigma_K(h) on K.

cgmt_aux_tr_cone_zero and cgmt_aux_tr_cone_ge are the same statements for a closed convex cone K and a set B of row vectors, with |proj K h| in place of sigma_K(h); tr_set0, tr_set_cone, tr_set_base, tr_set_sub and tr_set_norm_ge carry the hypotheses from row vectors to tr_set.

With the CGMT of cgmt.v: let a have law gauss (N * M), so that A = vec_mx a is an N x M matrix of independent standard normal entries, z have law gauss (N + M), g = lsubmx z and h = rsubmx z, N > 0, B be nonempty and |x| <= rho on B.

  • cone_escape_zero_tail: if rho > 0, K is closed, B is closed and convex and P(|g| < sigma_K(h)) > 1/2, then inf_(x in B) |A x| is at least rho (1 + 2 sqrt (ln 4)) + u with probability at most 2 exp (- u^2 / (2 rho^2)) (cgmt_zero_tail): the kernel of A meets K approximately.
  • cone_escape_lower_tail: if K is a cone, B is in K and r <= |x| on B, then inf_(x in B) |A x| is at most r E (|g| - sigma_K(h))_+ - rho - u with probability at most 2 exp (- u^2 / (2 rho^2)) (cgmt_lower and cgmt_escape_tail): the kernel of A stays away from B when |g| exceeds sigma_K(h) in mean by more than (rho + u) / r.
cone_sup K hsup_(x in K, |x| <= 1) <h, x>, for h : 'rV[R]_M

Main results

ResultsStatement
cone_supcone_sup_attainedcone_sup_dotcone_sup_lipschitzcone_sup_proj
For a set K of 'cV[R]_M containing 0, sigma_K(h) = sup_(x in K, |x| <= 1) <h, x> lies in [0, |h|], is 1-Lipschitz in h, and is attained when K is closed (compactness). For a cone K (a x in K for x in K and a >= 0), <h, x> <= |x| sigma_K(h) on K. For a closed convex cone K of row vectors, sigma_(tr_set K)(h) = |proj K h| (cone_proj_support).
cgmt_aux_cone_zerocgmt_aux_cone_gecgmt_aux_tr_cone_zerocgmt_aux_tr_cone_ge
The auxiliary value of the CGMT on a set B that contains a positive multiple of every nonzero point of a cone K: for K closed, cgmt_aux B g h = 0 when 0 < sigma_K(h) and |g| <= sigma_K(h), in particular when 0 < |g| <= sigma_K(h); for B nonempty and in K and r <= |x| on B, cgmt_aux B g h >= r (|g| - sigma_K(h))_+. The tr versions state the same for a closed convex cone and a set of row vectors, with |proj K h| in place of sigma_K(h).
cone_escape_zero_tailcone_escape_lower_tail
The CGMT on cones, for A = vec_mx a an N x M matrix of independent standard normal entries (N > 0), z = (g, h) of law gauss (N + M) and B as above, nonempty with |x| <= rho on B. If rho > 0, K is closed, B is closed and convex and P(|g| < sigma_K(h)) > 1/2, then inf_(x in B) |A x| >= rho (1 + 2 sqrt (ln 4)) + u has probability at most 2 exp (- u^2 / (2 rho^2)): the kernel of A meets K approximately. If B is in K and r <= |x| on B, then inf_(x in B) |A x| <= r E (|g| - sigma_K(h))_+ - rho - u has probability at most 2 exp (- u^2 / (2 rho^2)): the kernel stays away from B.

Declarations22 exported, 7 local

lemma, theoremdefinitioninstancelocal
sectioncone_sup
Context {R : realType} {M : nat}.
Variable K : set 'cV[R]_M.
definition cone_sup main result source, line 84
Type
forall {R : realType} {M : nat}, set 'cV_M -> 'rV_M -> R
Definition
Definition cone_sup (h : 'rV[R]_M) : R :=
  sup [set mxdot h^T x | x in [set x | K x /\ frobenius x <= 1]].

sigma_K(h) = sup_(x in K, |x| <= 1) <h, x>.

Main result, as the README states it

For a set K of 'cV[R]_M containing 0, sigma_K(h) = sup_(x in K, |x| <= 1) <h, x> lies in [0, |h|], is 1-Lipschitz in h, and is attained when K is closed (compactness). For a cone K (a x in K for x in K and a >= 0), <h, x> <= |x| sigma_K(h) on K. For a closed convex cone K of row vectors, sigma_(tr_set K)(h) = |proj K h| (cone_proj_support).

Used by 16 declarations in 1 file
let dot_le1 section-local source, line 87 
Let dot_le1 (h : 'rV[R]_M) (x : 'cV[R]_M) : frobenius x <= 1 ->
  mxdot h^T x <= frobenius h.
Used by 3 declarations in 1 file
lemma cone_sup_ub source, line 94 
forall {R : realType} {M : nat} [K : set 'cV_M] (h : 'rV_M) [x : 'cV_M],
K x -> frobenius x <= 1 -> mxdot h^T x <= cone_sup K h
Statement as written in the source
Lemma cone_sup_ub h x : K x -> frobenius x <= 1 -> mxdot h^T x <= cone_sup h.
Used by 4 declarations in 1 file
Hypothesis K0 : K 0.
lemma cone_sup_le source, line 102 
forall {R : realType} {M : nat} [K : set 'cV_M],
K 0 ->
forall [h : 'rV_M] [c : join_Num_NumDomain_between_GRing_ComNzRing_and_Order_Preorder R],
(forall x : 'cV_M, K x -> frobenius x <= 1 -> mxdot h^T x <= c) -> cone_sup K h <= c
Statement as written in the source
Lemma cone_sup_le h c :
  (forall x, K x -> frobenius x <= 1 -> mxdot h^T x <= c) -> cone_sup h <= c.
Used by 3 declarations in 1 file
lemma cone_sup_ge0 source, line 110 
forall {R : realType} {M : nat} [K : set 'cV_M], K 0 -> forall h : 'rV_M, 0 <= cone_sup K h
Statement as written in the source
Lemma cone_sup_ge0 h : 0 <= cone_sup h.
lemma cone_sup_le_norm source, line 116 
forall {R : realType} {M : nat} [K : set 'cV_M],
K 0 -> forall h : 'rV_M, cone_sup K h <= frobenius h
Statement as written in the source
Lemma cone_sup_le_norm h : cone_sup h <= frobenius h.
lemma cone_sup_lipschitz main result source, line 120 
forall {R : realType} {M : nat} [K : set 'cV_M],
K 0 -> forall h h' : 'rV_M, `|cone_sup K h - cone_sup K h'| <= frobenius (h - h')

sigma_K is 1-Lipschitz.

Main result

Stated in the README together with cone_sup.

Statement as written in the source
Lemma cone_sup_lipschitz h h' :
  `|cone_sup h - cone_sup h'| <= frobenius (h - h').
Used by 1 declaration in 1 file
lemma cone_sup_attained main result source, line 133 
forall {R : realType} {M : nat} [K : set 'cV_M],
K 0 ->
forall h : 'rV_M,
closed K -> exists x : 'cV_M, [/\ K x, frobenius x <= 1 & mxdot h^T x = cone_sup K h]

For K closed, the supremum is attained.

Main result

Stated in the README together with cone_sup.

Statement as written in the source
Lemma cone_sup_attained h : closed K ->
  exists x, [/\ K x, frobenius x <= 1 & mxdot h^T x = cone_sup h].
Used by 1 declaration in 1 file
Hypothesis Kcone : forall x (a : R), K x -> 0 <= a -> K (a *: x).
lemma cone_sup_dot main result source, line 168 
forall {R : realType} {M : nat} [K : set 'cV_M],
(forall (x : 'cV_M) (a : R), K x -> 0 <= a -> K (a *: x)) ->
forall (h : 'rV_M) [x : 'cV_M], K x -> mxdot h^T x <= frobenius x * cone_sup K h

On the cone, <h, x> <= |x| sigma_K(h).

Main result

Stated in the README together with cone_sup.

Statement as written in the source
Lemma cone_sup_dot h x : K x -> mxdot h^T x <= frobenius x * cone_sup h.
Used by 1 declaration in 1 file
sectioncone_sup_proj
Context {R : realType} {M : nat}.
Variable K : set 'rV[R]_M.
lemma cone_sup_tr_setE source, line 186 
forall {R : realType} {M : nat} (K : set 'rV_M) (h : 'rV_M),
cone_sup (tr_set K) h = sup [set mxdot h y | y in [set y | K y /\ frobenius y <= 1]]
Statement as written in the source
Lemma cone_sup_tr_setE (h : 'rV[R]_M) :
  cone_sup (tr_set K) h =
  sup [set mxdot h y | y in [set y | K y /\ frobenius y <= 1]].
Used by 1 declaration in 1 file
Hypotheses (Kc : closed K) (K0 : K 0).
Hypothesis Kcvx : forall x y (t : R), K x -> K y -> 0 <= t <= 1 ->
  K (x + t *: (y - x)).
Hypothesis Kcone : forall y (a : R), K y -> 0 <= a -> K (a *: y).
lemma cone_sup_proj main result source, line 203 
forall {R : realType} {M : nat} [K : set 'rV_M],
closed K ->
K 0 ->
(forall (x y : 'rV_M) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
(forall (y : 'rV_M) (a : R), K y -> 0 <= a -> K (a *: y)) ->
forall h : 'rV_M, cone_sup (tr_set K) h = frobenius (proj K h)

For a closed convex cone, sigma is the norm of the projection.

Main result

Stated in the README together with cone_sup.

Statement as written in the source
Lemma cone_sup_proj (h : 'rV[R]_M) :
  cone_sup (tr_set K) h = frobenius (proj K h).
Used by 2 declarations in 1 file
sectiontr_set_cone
Context {R : realType} {M : nat}.
Variables (K B : set 'rV[R]_M).
lemma tr_set0 source, line 219 
forall {R : realType} {M : nat} [K : set 'rV_M], K 0 -> tr_set K 0
Statement as written in the source
Lemma tr_set0 : K 0 -> tr_set K 0.
Used by 1 declaration in 1 file
lemma tr_set_cone source, line 222 
forall {R : realType} {M : nat} [K : set 'rV_M],
(forall (y : 'rV_M) (a : R), K y -> 0 <= a -> K (a *: y)) ->
forall [x : 'cV_M] [a : R], tr_set K x -> 0 <= a -> tr_set K (a *: x)
Statement as written in the source
Lemma tr_set_cone : (forall y (a : R), K y -> 0 <= a -> K (a *: y)) ->
  forall x (a : R), tr_set K x -> 0 <= a -> tr_set K (a *: x).
Used by 1 declaration in 1 file
lemma tr_set_base source, line 229 
forall {R : realType} {M : nat} [K B : set 'rV_M],
(forall y : 'rV_M, K y -> y != 0 -> exists2 a : R, 0 < a & B (a *: y)) ->
forall [x : 'cV_M], tr_set K x -> x != 0 -> exists2 a : R, 0 < a & tr_set B (a *: x)
Statement as written in the source
Lemma tr_set_base :
  (forall y, K y -> y != 0 -> exists2 a : R, 0 < a & B (a *: y)) ->
  forall x, tr_set K x -> x != 0 -> exists2 a : R, 0 < a & tr_set B (a *: x).
Used by 1 declaration in 1 file
lemma tr_set_sub source, line 239 
forall {R : realType} {M : nat} [K B : set 'rV_M],
(forall y : 'rV_M, B y -> K y) -> forall [x : 'cV_M], tr_set B x -> tr_set K x
Statement as written in the source
Lemma tr_set_sub : (forall y, B y -> K y) ->
  forall x, tr_set B x -> tr_set K x.
Used by 1 declaration in 1 file
lemma tr_set_norm_ge source, line 243 
forall {R : realType} {M : nat} [B : set 'rV_M] [r : R],
(forall y : 'rV_M, B y -> r <= frobenius y) ->
forall [x : 'cV_M], tr_set B x -> r <= frobenius x
Statement as written in the source
Lemma tr_set_norm_ge (r : R) : (forall y, B y -> r <= frobenius y) ->
  forall x, tr_set B x -> r <= frobenius x.
Used by 1 declaration in 1 file
sectioncone_aux
Context {R : realType} {N M : nat}.
Variables (K B : set 'cV[R]_M).
Hypothesis K0 : K 0.
sectionzero
Hypothesis Kc : closed K.
Hypothesis Bbase : forall x, K x -> x != 0 -> exists2 a : R, 0 < a & B (a *: x).
lemma cgmt_aux_cone_zero main result source, line 259 
forall {R : realType} {N M : nat} [K B : set 'cV_M],
K 0 ->
closed K ->
(forall x : 'cV_M, K x -> x != 0 -> exists2 a : R, 0 < a & B (a *: x)) ->
forall [g : 'rV_N] [h : 'rV_M],
0 < cone_sup K h -> frobenius g <= cone_sup K h -> cgmt_aux B g h = 0

phi(B) = 0 when 0 < sigma_K(h) and |g| <= sigma_K(h).

Main result, as the README states it

The auxiliary value of the CGMT on a set B that contains a positive multiple of every nonzero point of a cone K: for K closed, cgmt_aux B g h = 0 when 0 < sigma_K(h) and |g| <= sigma_K(h), in particular when 0 < |g| <= sigma_K(h); for B nonempty and in K and r <= |x| on B, cgmt_aux B g h >= r (|g| - sigma_K(h))_+. The tr versions state the same for a closed convex cone and a set of row vectors, with |proj K h| in place of sigma_K(h).

Statement as written in the source
Lemma cgmt_aux_cone_zero (g : 'rV[R]_N) (h : 'rV[R]_M) :
  0 < cone_sup K h -> frobenius g <= cone_sup K h -> cgmt_aux B g h = 0.
Used by 2 declarations in 1 file
lemma cgmt_aux_cone_zero_lt source, line 275 
forall {R : realType} {N M : nat} [K B : set 'cV_M],
K 0 ->
closed K ->
(forall x : 'cV_M, K x -> x != 0 -> exists2 a : R, 0 < a & B (a *: x)) ->
forall [g : 'rV_N] [h : 'rV_M], frobenius g < cone_sup K h -> cgmt_aux B g h = 0
Statement as written in the source
Lemma cgmt_aux_cone_zero_lt (g : 'rV[R]_N) (h : 'rV[R]_M) :
  frobenius g < cone_sup K h -> cgmt_aux B g h = 0.
Used by 1 declaration in 1 file
sectionlower
Hypothesis Kcone : forall x (a : R), K x -> 0 <= a -> K (a *: x).
Hypothesis BK : forall x, B x -> K x.
Variable r : R.
Hypothesis Br : forall x, B x -> r <= frobenius x.
lemma cgmt_aux_cone_ge main result source, line 291 
forall {R : realType} {N M : nat} [K B : set 'cV_M],
(forall (x : 'cV_M) (a : R), K x -> 0 <= a -> K (a *: x)) ->
(forall x : 'cV_M, B x -> K x) ->
forall [r : R],
(forall x : 'cV_M, B x -> r <= frobenius x) ->
forall (g : 'rV_N) (h : 'rV_M),
B !=set0 -> r * maxr 0 (frobenius g - cone_sup K h) <= cgmt_aux B g h

phi(B) >= r (|g| - sigma_K(h))_+.

Main result

Stated in the README together with cgmt_aux_cone_zero.

Statement as written in the source
Lemma cgmt_aux_cone_ge (g : 'rV[R]_N) (h : 'rV[R]_M) : B !=set0 ->
  r * Num.max 0 (frobenius g - cone_sup K h) <= cgmt_aux B g h.
Used by 2 declarations in 1 file
sectioncone_aux_rows
Context {R : realType} {N M : nat}.
Variables (K B : set 'rV[R]_M).
Hypotheses (Kc : closed K) (K0 : K 0).
Hypothesis Kcvx : forall x y (t : R), K x -> K y -> 0 <= t <= 1 ->
  K (x + t *: (y - x)).
Hypothesis Kcone : forall y (a : R), K y -> 0 <= a -> K (a *: y).
corollary cgmt_aux_tr_cone_zero main result source, line 320 
forall {R : realType} {N M : nat} [K B : set 'rV_M],
closed K ->
K 0 ->
(forall (x y : 'rV_M) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
(forall (y : 'rV_M) (a : R), K y -> 0 <= a -> K (a *: y)) ->
forall [g : 'rV_N] [h : 'rV_M],
(forall y : 'rV_M, K y -> y != 0 -> exists2 a : R, 0 < a & B (a *: y)) ->
0 < frobenius g -> frobenius g <= frobenius (proj K h) -> cgmt_aux (tr_set B) g h = 0

(i) for row vectors: phi(B) = 0 when 0 < |g| <= |proj K h|.

Main result

Stated in the README together with cgmt_aux_cone_zero.

Statement as written in the source
Corollary cgmt_aux_tr_cone_zero (g : 'rV[R]_N) (h : 'rV[R]_M) :
  (forall y, K y -> y != 0 -> exists2 a : R, 0 < a & B (a *: y)) ->
  0 < frobenius g -> frobenius g <= frobenius (proj K h) ->
  cgmt_aux (tr_set B) g h = 0.
corollary cgmt_aux_tr_cone_ge main result source, line 332 
forall {R : realType} {N M : nat} [K B : set 'rV_M],
closed K ->
K 0 ->
(forall (x y : 'rV_M) (t : R), K x -> K y -> 0 <= t <= 1 -> K (x + t *: (y - x))) ->
(forall (y : 'rV_M) (a : R), K y -> 0 <= a -> K (a *: y)) ->
forall [r : R] (g : 'rV_N) (h : 'rV_M),
B !=set0 ->
(forall y : 'rV_M, B y -> K y) ->
(forall y : 'rV_M, B y -> r <= frobenius y) ->
r * maxr 0 (frobenius g - frobenius (proj K h)) <= cgmt_aux (tr_set B) g h

(ii) for row vectors: phi(B) >= r (|g| - |proj K h|)_+.

Main result

Stated in the README together with cgmt_aux_cone_zero.

Statement as written in the source
Corollary cgmt_aux_tr_cone_ge (r : R) (g : 'rV[R]_N) (h : 'rV[R]_M) :
  B !=set0 -> (forall y, B y -> K y) -> (forall y, B y -> r <= frobenius y) ->
  r * Num.max 0 (frobenius g - frobenius (proj K h)) <=
  cgmt_aux (tr_set B) g h.
sectioncone_escape
Context {R : realType} {N M : nat}.
Variables (K B : set 'cV[R]_M) (rho : R).
Hypotheses (K0 : K 0) (B0 : B !=set0).
Hypothesis Bb : forall x, B x -> frobenius x <= rho.
let F section-local source, line 352 
Let F (z : 'rV[R]_(N + M)) : R := frobenius (lsubmx z) - cone_sup K (rsubmx z).

|g| - sigma_K(h) is a Lipschitz function of z = (g, h).

Used by 5 declarations in 1 file
let F_lip section-local source, line 354 
Let F_lip (z z' : 'rV[R]_(N + M)) :
  `|F z - F z'| <= Num.sqrt 2 * frobenius (z - z').
Used by 2 declarations in 1 file
let F0_lip section-local source, line 366 
Let F0_lip (z z' : 'rV[R]_(N + M)) :
  `|Num.max 0 (F z) - Num.max 0 (F z')| <= Num.sqrt 2 * frobenius (z - z').
Used by 1 declaration in 1 file
let mF section-local source, line 377 
Let mF : measurable_fun setT F.
Used by 1 declaration in 1 file
let mphi section-local source, line 382 
Let mphi : measurable_fun setT
  (fun z : 'rV[R]_(N + M) => cgmt_aux B (lsubmx z) (rsubmx z)).
Used by 1 declaration in 1 file
let mPhi section-local source, line 386 
Let mPhi : measurable_fun setT
  (fun a : 'rV[R]_(N * M) => escape_inf B (vec_mx a : 'M[R]_(N, M))).
Used by 1 declaration in 1 file
theorem cone_escape_zero_tail main result source, line 394 
forall {R : realType} {N M : nat} [K B : set 'cV_M] [rho : R],
K 0 ->
B !=set0 ->
(forall x : 'cV_M, B x -> frobenius x <= rho) ->
forall [u : R],
(0 < N)%N ->
0 < rho ->
closed K ->
(forall x : 'cV_M, K x -> x != 0 -> exists2 a : R, 0 < a & B (a *: x)) ->
closed B ->
(forall (x y : 'cV_M) (t : R), B x -> B y -> 0 <= t <= 1 -> B (x + t *: (y - x))) ->
0 <= u ->
((2^-1)%:E < gauss (N + M) [set z | (frobenius (lsubmx z) < cone_sup K (rsubmx z))%R])%E ->
(gauss (N * M)
   [set a | (rho * (1 + 2 * Num.ExtraDef.sqrtr (ln 4)) + u <=
             escape_inf B (vec_mx a : 'M_(N, M)))%R] <=
 (2 * expR (- u ^+ 2 / (2 * rho ^+ 2)))%:E)%E

If |g| < sigma_K(h) with probability more than 1/2, the kernel of A meets K approximately: inf_(x in B) |A x| is at least rho (1 + 2 sqrt (ln 4)) + u with probability at most 2 exp (- u^2 / (2 rho^2)).

Main result, as the README states it

The CGMT on cones, for A = vec_mx a an N x M matrix of independent standard normal entries (N > 0), z = (g, h) of law gauss (N + M) and B as above, nonempty with |x| <= rho on B. If rho > 0, K is closed, B is closed and convex and P(|g| < sigma_K(h)) > 1/2, then inf_(x in B) |A x| >= rho (1 + 2 sqrt (ln 4)) + u has probability at most 2 exp (- u^2 / (2 rho^2)): the kernel of A meets K approximately. If B is in K and r <= |x| on B, then inf_(x in B) |A x| <= r E (|g| - sigma_K(h))_+ - rho - u has probability at most 2 exp (- u^2 / (2 rho^2)): the kernel stays away from B.

Statement as written in the source
Theorem cone_escape_zero_tail (u : R) : (0 < N)%N -> 0 < rho ->
  closed K ->
  (forall x, K x -> x != 0 -> exists2 a : R, 0 < a & B (a *: x)) ->
  closed B ->
  (forall x y (t : R), B x -> B y -> 0 <= t <= 1 -> B (x + t *: (y - x))) ->
  0 <= u ->
  ((2^-1)%:E <
    gauss (N + M) [set z | frobenius (lsubmx z) < cone_sup K (rsubmx z)]%R)%E ->
  (gauss (N * M) [set a | rho * (1 + 2 * Num.sqrt (ln 4)) + u <=
     escape_inf B (vec_mx a : 'M[R]_(N, M))]%R <=
   (2 * expR (- u ^+ 2 / (2 * rho ^+ 2)))%:E)%E.
theorem cone_escape_lower_tail main result source, line 420 
forall {R : realType} {N M : nat} [K B : set 'cV_M] [rho : R],
K 0 ->
B !=set0 ->
(forall x : 'cV_M, B x -> frobenius x <= rho) ->
forall [r u : R],
(0 < N)%N ->
(forall (x : 'cV_M) (a : R), K x -> 0 <= a -> K (a *: x)) ->
(forall x : 'cV_M, B x -> K x) ->
(forall x : 'cV_M, B x -> r <= frobenius x) ->
0 <= u ->
(gauss (N * M)
   [set a | (escape_inf B (vec_mx a : 'M_(N, M)) <=
             r *
             \int[gauss (N + M)]_z maxr 0 (frobenius (lsubmx z) - cone_sup K (rsubmx z)) -
             rho - u)%R] <=
 (2 * expR (- u ^+ 2 / (2 * rho ^+ 2)))%:E)%E

The kernel of A stays away from B: inf_(x in B) |A x| is at most r E (|g| - sigma_K(h))_+ - rho - u with probability at most 2 exp (- u^2 / (2 rho^2)).

Main result

Stated in the README together with cone_escape_zero_tail.

Statement as written in the source
Theorem cone_escape_lower_tail (r u : R) : (0 < N)%N ->
  (forall x (a : R), K x -> 0 <= a -> K (a *: x)) ->
  (forall x, B x -> K x) -> (forall x, B x -> r <= frobenius x) -> 0 <= u ->
  (gauss (N * M) [set a | escape_inf B (vec_mx a : 'M[R]_(N, M)) <=
     r * \int[gauss (N + M)]_z
       Num.max 0 (frobenius (lsubmx z) - cone_sup K (rsubmx z)) - rho - u]%R <=
   (2 * expR (- u ^+ 2 / (2 * rho ^+ 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.