GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisrandom_matrixrestricted_isometry

Restricted isometry of matrices with independent psi_1 columns

GaussianAnalysis.random_matrix.restricted_isometrylibrary/random_matrix/restricted_isometry.v2,547 lines113 lemmas and theorems, 40 definitionssource
Imports 8 library modules and 23 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.numfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability

Required by 9 files of the paper proofs

Theorem 5.1 of Adamczak, Litvak, Pajor and Tomczak-Jaegermann (Constr. Approx. 2011, arXiv 0904.4723) at r = 1, with explicit constants: the off-diagonal part of the Gram matrix of independent centered psi_1 vectors is small on sparse vectors. Koehler and Sohn (arXiv 2608.27372, lines 2192-2221) cite it for the a priori estimates of their Proposition 3.1. With it, the norms of sparse combinations of independent subgaussian vectors (their second a priori estimate).

Setting: x_1, ..., x_N in 'rV[R]_n are the coordinates of x of law tuple_prod mu N, and every linear form <x_i, y>, |y| = 1, is centered and subexponential with constant psi under mu i. The rows of tuple_mx x are the x_i, so u *m tuple_mx x = sum_i u_i x_i.

tuple_mx xthe N x n matrix with rows x_1, ..., x_N
supp uthe support of u : 'rV[R]_N
restr E uu restricted to the coordinates in E
gram_off x u v<u X, v X> - sum_i u_i v_i |x_i|^2, the off-diagonal part of the Gram form, sum_(i <> j) u_i v_j <x_i, x_j>
maxnorm xmax_i |x_i|
sparse_ball mthe m-sparse vectors of norm at most 1
rip_const m xB_m^2 = sup over sparse_ball m of |gram_off x u u|
rip_T beta K2100 K psi sqrt m (ln (e N / m) + ln (1 / beta))
sqnorm_dev xmax_i | |x_i|^2 - 1 |
sparse_emb wthe vector supported in F with coordinates w, for w : 'cV_#|F| (in the order of enum_val)
sparse_proj F zthe coordinates of z in F
tuple_submx F xthe n x |F| matrix with columns x_i, i in F
sphere_net ka 1/4-net of the unit sphere of 'cV_k of size at most (18 e)^k
sparse_norm_bound m s8 K sqrt (m (1 + ln (N / m)) + 6 (m + n) + s)

Main results:

  • restricted_isometry: for 1 <= m <= N, 0 < beta <= 1/2 and K >= 1, there is a measurable event G with P(not G) <= 2 (log_4 m + 2) exp (- K sqrt m ln (e N / m)) on which B_m^2 <= 256 T^2 + 32 T C + 8 beta C^2, T = rip_T beta K and C = maxnorm x. Hence |u X|^2 - sum_i u_i^2 |x_i|^2 is at most this bound times |u|^2 for every m-sparse u (gram_off_rip).
  • sparse_isometry_dev: | |u X|^2 - |u|^2 | <= (B_m^2 + sqnorm_dev x) |u|^2 for every m-sparse u, which bounds the restricted isometry constant.
  • tuple_mx_blocks: if |u X| <= L |u| for every m-sparse u, then |u X| <= L sqrt (N %/ m + 1) |u| for every u (blocks of m indices).
  • sparse_norm_subgaussian: if the linear forms of the x_i are centered and subgaussian with constant K, then with probability at least 1 - 2 exp (- s), |u X| <= sparse_norm_bound m s |u| for every m-sparse u: Hoeffding's inequality for a fixed pair (tuple_mx_dot_tail), nets of both unit spheres (tuple_submx_net) and a union bound over the supports.

The proof of restricted_isometry, after ALPT with value levels instead of sorted coordinates:

  • cross_tail: for a and b with disjoint supports, |a| <= 1 and |a_i| <= al, P(|<a X, b X>| > t |b X|) <= 2 exp (- min (t^2 / (64 psi^2), t / (4 al psi))), by Bernstein's inequality conditionally on the vectors in the support of b (tuple_prod_cond_le of conditioning.v);
  • gram_off_decouple: the off-diagonal form is an average of decoupled forms <restr E y X, restr (F \ E) y X> over the subsets E of F;
  • the levels of z: level k collects the coordinates with 4^(k-1) < m z_i^2 <= 4^k; it has at most lsize k elements, each at most alpha k = 2^k / sqrt m (level_size, level_alpha), and z is the sum of its restrictions to the levels (level_sum);
  • sparse_net: nets of the vectors supported in F with sup norm at most al, of size exponential in |F|; small_sets_le: there are at most (e N / s)^s sets of size at most s;
  • rip_const_le: if every decoupled diagonal term of level k and every term of level k against the levels above (upper) is at most t k times the norm of its second vector, then B_m^2 <= 256 T^2 + 32 T C + 8 beta C^2 with T = sum_k t k (the approximation by nets, the triangular expansion gram_off_tri and the bound A_m^2 <= B_m^2 + C^2 in place of the A_m of ALPT);
  • bad_event_le, conf_size, tk_exp: the union bound over the finite lists wconf k and xconf k of configurations, whose sizes are at most 2 exp (2 H_k) with H_k = (4 m / 4^k) (9 + ln (N / m) - ln beta + 3 k) (ccount_le); tk_sum: the thresholds t k sum to at most rip_T beta K.

Main results

ResultsStatement
restricted_isometryrip_constrip_T
Theorem 5.1 of Adamczak, Litvak, Pajor and Tomczak-Jaegermann at r = 1, with explicit constants. Let x_1, ..., x_N in 'rV[R]_n be independent (tuple_prod mu N), with every linear form <x_i, y>, |y| = 1, centered and subexponential with constant psi. For 1 <= m <= N, 0 < beta <= 1/2 and K >= 1, outside a measurable event of probability at most 2 (log_4 m + 2) exp (- K sqrt m (1 + ln (N / m))), every m-sparse u of norm at most one satisfies ||sum_i u_i x_i|^2 - sum_i u_i^2 |x_i|^2| <= 256 T^2 + 32 T C + 8 beta C^2, where T = 2100 K psi sqrt m (1 + ln (N / m) - ln beta) and C = max_i |x_i|.
gram_off_riptuple_mx_ripgram_off_rip2
With B^2 = rip_const m x (the supremum above) and C = max_i |x_i|, for all m-sparse u and v: |gram_off x u u| <= B^2 |u|^2, |sum_i u_i x_i| <= sqrt (B^2 + C^2) |u| and |gram_off x u v| <= (B^2 + 2 C^2) |u| |v|, where gram_off x u v = sum_(i <> j) u_i v_j <x_i, x_j>.
cross_tail
For a and b in 'rV[R]_N with disjoint supports, |a| <= 1 and |a_i| <= al for all i, and t > 0: P(|<sum_i a_i x_i, sum_j b_j x_j>| > t |sum_j b_j x_j|) <= 2 exp (- min (t^2 / (64 psi^2), t / (4 al psi))), by Bernstein's inequality conditionally on the vectors in the support of b.
gram_off_decouplesparse_netsmall_sets_le
Decoupling: if y is supported in F and |<sum_(i in E) y_i x_i, sum_(j in F \ E) y_j x_j>| <= c for every E included in F, then |gram_off x y y| <= 4 c. Nets: the vectors supported in F with norm at most one and coordinates at most al have an eps-net of at most (2 e (1 + 2 / eps))^|F| points. Counting: there are at most (e N / s)^s subsets of {1, ..., N} with at most s elements, for 1 <= s <= N.
sparse_isometry_devsqnorm_devtuple_mx_blocks
The restricted isometry constant: for every m-sparse u, ||sum_i u_i x_i|^2 - |u|^2| <= (rip_const m x + max_i ||x_i|^2 - 1|) |u|^2. Blocks: if |sum_i u_i x_i| <= L |u| for every m-sparse u, then |sum_i u_i x_i| <= L sqrt (N / m + 1) |u| for every u (deterministic).
sparse_norm_subgaussiansparse_norm_boundtuple_mx_dot_tail
Norms of sparse combinations of independent subgaussian vectors: if x_1, ..., x_N in 'rV[R]_n are independent (tuple_prod mu N) with every linear form <x_i, y>, |y| = 1, centered and subgaussian with constant K, then for 1 <= m <= N and s >= 0, outside a measurable event of probability at most 2 exp (- s), every m-sparse u satisfies |sum_i u_i x_i| <= 8 K sqrt (m (1 + ln (N / m)) + 6 (m + n) + s) |u| (Vershynin's Theorem 4.4.5 with a union bound over the supports). For unit a and y, P(|<sum_i a_i x_i, y>| >= t) <= 2 exp (- t^2 / (16 K^2)).

Declarations153 exported, 5 local

lemma, theoremdefinitioninstancelocal
sectioncolumns
Context {R : realType} (N n : nat).
Implicit Types (x : N.-tuple 'rV[R]_n) (u v a b : 'rV[R]_N).
definition tuple_mx source, line 108
Type
forall {R : realType} [N n : nat], N.-tuple 'rV_n -> 'M_(N, n)
Definition
Definition tuple_mx x : 'M[R]_(N, n) := \matrix_(i, j) (tnth x i) 0 j.

The N x n matrix whose rows are the vectors of x: u *m tuple_mx x is the combination sum_i u_i x_i.

Used by 20 declarations in 1 file
definition supp source, line 110
Type
forall {R : realType} [N : nat], 'rV_N -> {set 'I_N}
Definition
Definition supp u : {set 'I_N} := [set i | u 0 i != 0].
Used by 21 declarations in 1 file
definition restr source, line 112
Type
forall {R : realType} [N : nat], {set 'I_N} -> 'rV_N -> 'rV_N
Definition
Definition restr (E : {set 'I_N}) u : 'rV[R]_N :=
  \row_i (if i \in E then u 0 i else 0).
Used by 16 declarations in 1 file
definition gram_off source, line 117
Type
forall {R : realType} [N n : nat], N.-tuple 'rV_n -> 'rV_N -> 'rV_N -> R
Definition
Definition gram_off x u v : R :=
  mxdot (u *m tuple_mx x) (v *m tuple_mx x) -
  \sum_i u 0 i * v 0 i * mxdot (tnth x i) (tnth x i).

The off-diagonal part of the Gram form: <u X, v X> - sum_i u_i v_i |x_i|^2, that is sum_(i <> j) u_i v_j <x_i, x_j>.

Used by 19 declarations in 1 file
definition maxnorm source, line 121
Type
forall {R : realType} [N n : nat], N.-tuple 'rV_n -> R
Definition
Definition maxnorm x : R := \big[Num.max/0]_i frobenius (tnth x i).
Used by 8 declarations in 1 file
lemma tuple_mxE source, line 123 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (u : 'rV_N),
u *m tuple_mx x = \sum_i u 0 i *: tnth x i
Statement as written in the source
Lemma tuple_mxE x u : u *m tuple_mx x = \sum_i u 0 i *: tnth x i.
Used by 4 declarations in 1 file
lemma mxdot_tuple_mx source, line 129 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (u v : 'rV_N),
mxdot (u *m tuple_mx x) (v *m tuple_mx x) =
\sum_i \sum_j u 0 i * v 0 j * mxdot (tnth x i) (tnth x j)
Statement as written in the source
Lemma mxdot_tuple_mx x u v : mxdot (u *m tuple_mx x) (v *m tuple_mx x) =
  \sum_i \sum_j u 0 i * v 0 j * mxdot (tnth x i) (tnth x j).
Used by 2 declarations in 1 file
lemma gram_offE source, line 137 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (u v : 'rV_N),
gram_off x u v = \sum_i \sum_(j | j != i) u 0 i * v 0 j * mxdot (tnth x i) (tnth x j)
Statement as written in the source
Lemma gram_offE x u v : gram_off x u v =
  \sum_i \sum_(j | j != i) u 0 i * v 0 j * mxdot (tnth x i) (tnth x j).
Used by 2 declarations in 1 file
lemma supp_restr source, line 144 
forall {R : realType} [N : nat] (E : {set 'I_N}) (u : 'rV_N),
supp (restr E u) = E :&: supp u
Statement as written in the source
Lemma supp_restr E u : supp (restr E u) = E :&: supp u.
Used by 1 declaration in 1 file
lemma restrE source, line 149 
forall {R : realType} [N : nat] (E : {set 'I_N}) (u : 'rV_N) (i : 'I_N),
restr E u 0 i = (if i \in E then u 0 i else 0)
Statement as written in the source
Lemma restrE E u i : restr E u 0 i = if i \in E then u 0 i else 0.
Used by 8 declarations in 1 file
lemma restr_supp source, line 152 
forall {R : realType} [N : nat] [E : {set 'I_N}] [u : 'rV_N],
supp u \subset E -> restr E u = u
Statement as written in the source
Lemma restr_supp (E : {set 'I_N}) u : supp u \subset E -> restr E u = u.
Used by 1 declaration in 1 file
lemma maxnorm_ge0 source, line 159 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n), 0 <= maxnorm x
Statement as written in the source
Lemma maxnorm_ge0 x : 0 <= maxnorm x.
Used by 5 declarations in 1 file
lemma card_supp0 source, line 164 
forall {R : realType} (N : nat), #|supp (0 : 'rV_N)| = 0%N
Statement as written in the source
Lemma card_supp0 : #|supp (0 : 'rV[R]_N)| = 0%N.
Used by 2 declarations in 1 file
definition disj source, line 168
Type
forall {R : realType} [N : nat], 'rV_N -> 'rV_N -> Prop
Definition
Definition disj u v := forall i, u 0 i = 0 \/ v 0 i = 0.

u and v have disjoint supports.

Used by 8 declarations in 1 file
lemma gram_off_disj source, line 171 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) [a b : 'rV_N],
disj a b -> gram_off x a b = mxdot (a *m tuple_mx x) (b *m tuple_mx x)

Two vectors with disjoint supports: the diagonal terms vanish.

Statement as written in the source
Lemma gram_off_disj x a b : disj a b ->
  gram_off x a b = mxdot (a *m tuple_mx x) (b *m tuple_mx x).
Used by 1 declaration in 1 file
sectionmeasurability
Context {R : realType} (N n : nat).
lemma measurable_tuple_mx_comb source, line 183 
forall {R : realType} [N n : nat] (a : 'rV_N),
measurable_fun [set: N.-tuple 'rV_n]
  (fun x : N.-tuple _ => a *m tuple_mx x)
Statement as written in the source
Lemma measurable_tuple_mx_comb (a : 'rV[R]_N) :
  measurable_fun [set: N.-tuple 'rV[R]_n] (fun x => a *m tuple_mx x).
Used by 2 declarations in 1 file
lemma measurable_mxdot_comb source, line 194 
forall {R : realType} [N n : nat] [f g : N.-tuple 'rV_n -> 'rV_n],
measurable_fun [set: N.-tuple _] f ->
measurable_fun [set: N.-tuple _] g ->
measurable_fun [set: N.-tuple 'rV_n]
  (fun x : N.-tuple _ => mxdot (f x) (g x))
Statement as written in the source
Lemma measurable_mxdot_comb (f g : N.-tuple 'rV[R]_n -> 'rV[R]_n) :
  measurable_fun setT f -> measurable_fun setT g ->
  measurable_fun [set: N.-tuple 'rV[R]_n] (fun x => mxdot (f x) (g x)).
Used by 2 declarations in 1 file
definition cross_event source, line 206
Type
forall {R : realType} [N n : nat], R -> 'rV_N -> 'rV_N -> set (N.-tuple 'rV_n)
Definition
Definition cross_event (t : R) (a b : 'rV[R]_N) : set (N.-tuple 'rV[R]_n) :=
  [set x | t * frobenius (b *m tuple_mx x) <
           `|mxdot (a *m tuple_mx x) (b *m tuple_mx x)|].

The event that <a X, b X> exceeds t |b X|.

Used by 3 declarations in 1 file
lemma measurable_cross_event source, line 210 
forall {R : realType} [N n : nat]
  [t : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R]
  (a b : 'rV_N),
0 <= t ->
(measure_tuple_display (measure_matrix_display default_measure_display)).-measurable
  (cross_event t a b)
Statement as written in the source
Lemma measurable_cross_event t a b : 0 <= t -> measurable (cross_event t a b).
Used by 3 declarations in 1 file
sectioncross_tail
Context {R : realType} (N n : nat) (mu : nat -> probability 'rV[R]_n R)
  (psi : R).
Hypothesis psi0 : 0 < psi.

The columns are centered psi_1 vectors.

Hypothesis sub : forall i (y : 'rV[R]_n), (i < N)%N -> mxdot y y = 1 ->
  subexponential (mu i) (fun v => mxdot v y) psi.
Hypothesis cen : forall i (y : 'rV[R]_n), (i < N)%N -> mxdot y y = 1 ->
  \int[mu i]_v mxdot v y = 0.
let coef section-local source, line 241 
Let coef (a : 'rV[R]_N) (k : nat) : R :=
  if insub k is Some i then a 0 i else 0.
Used by 2 declarations in 1 file
let coefE section-local source, line 244 
Let coefE (a : 'rV[R]_N) (i : 'I_N) : coef a i = a 0 i.
Used by 1 declaration in 1 file
lemma cross_tail main result source, line 249 
forall {R : realType} [N n : nat] [mu : nat -> probability 'rV_n R] [psi : R],
0 < psi ->
(forall (i : nat) (y : 'rV_n),
 (i < N)%N -> mxdot y y = 1 -> subexponential (mu i) ((mxdot (n:=n))^~ y) psi) ->
(forall (i : nat) (y : 'rV_n), (i < N)%N -> mxdot y y = 1 -> \int[mu i]_v mxdot v y = 0) ->
forall [a b : 'rV_N] [al t : R],
disj a b ->
mxdot a a <= 1 ->
(forall i : 'I_N, `|a 0 i| <= al) ->
0 < t ->
(tuple_prod mu N (cross_event t a b) <=
 (2 * expR (- minr (t ^+ 2 / (64 * psi ^+ 2)) (t / (4 * (al * psi)))))%:E)%E

Conditionally on the vectors in the support of b, <a X, b X> is a sum of independent centered psi_1 variables: Bernstein's inequality.

Main result, as the README states it

For a and b in 'rV[R]_N with disjoint supports, |a| <= 1 and |a_i| <= al for all i, and t > 0: P(|<sum_i a_i x_i, sum_j b_j x_j>| > t |sum_j b_j x_j|) <= 2 exp (- min (t^2 / (64 psi^2), t / (4 al psi))), by Bernstein's inequality conditionally on the vectors in the support of b.

Statement as written in the source
Lemma cross_tail (a b : 'rV[R]_N) (al t : R) : disj a b ->
  mxdot a a <= 1 -> (forall i, `|a 0 i| <= al) -> 0 < t ->
  (tuple_prod mu N (cross_event t a b) <=
   (2 * expR (- Num.min (t ^+ 2 / (64 * psi ^+ 2))
                        (t / (4 * (al * psi)))))%:E)%E.
Used by 1 declaration in 1 file
sectiondecoupling
Context {R : realType} (N n : nat).
Implicit Types (x : N.-tuple 'rV[R]_n) (y : 'rV[R]_N).
lemma sum_ffun_sel source, line 366 
forall {R : realType} [N : nat] [i j : 'I_N],
i != j -> 4 * \sum_f ((f i && ~~ f j)%:R : R) = 2 ^+ N

For i <> j, a uniform random subset contains i and not j with probability 1/4.

Statement as written in the source
Lemma sum_ffun_sel (i j : 'I_N) : i != j ->
  4 * \sum_(f : {ffun 'I_N -> bool}) ((f i && ~~ f j)%:R : R) = 2 ^+ N.
Used by 1 declaration in 1 file
lemma gram_off_decouple main result source, line 392 
forall {R : realType} [N n : nat] [x : N.-tuple 'rV_n] [F : {set 'I_N}] [y : 'rV_N] [c : R],
supp y \subset F ->
(forall E : {set 'I_N},
 E \subset F -> `|mxdot (restr E y *m tuple_mx x) (restr (F :\: E) y *m tuple_mx x)| <= c) ->
`|gram_off x y y| <= 4 * c

The off-diagonal Gram form is an average of decoupled forms.

Main result, as the README states it

Decoupling: if y is supported in F and |<sum_(i in E) y_i x_i, sum_(j in F \ E) y_j x_j>| <= c for every E included in F, then |gram_off x y y| <= 4 c. Nets: the vectors supported in F with norm at most one and coordinates at most al have an eps-net of at most (2 e (1 + 2 / eps))^|F| points. Counting: there are at most (e N / s)^s subsets of {1, ..., N} with at most s elements, for 1 <= s <= N.

Statement as written in the source
Lemma gram_off_decouple x (F : {set 'I_N}) y (c : R) :
  supp y \subset F ->
  (forall E : {set 'I_N}, E \subset F ->
    `|mxdot (restr E y *m tuple_mx x)
            (restr (F :\: E) y *m tuple_mx x)| <= c) ->
  `|gram_off x y y| <= 4 * c.
Used by 1 declaration in 1 file
sectionsparse_nets
Context {R : realType} (N : nat).
definition sball source, line 465
Type
forall {R : realType} [N : nat], {set 'I_N} -> R -> set 'rV_N
Definition
Definition sball (F : {set 'I_N}) (al : R) : set 'rV[R]_N :=
  [set y | [/\ supp y \subset F, mxdot y y <= 1 & forall i, `|y 0 i| <= al]].

The vectors supported in F of norm at most 1 with coordinates at most al in absolute value.

Used by 3 declarations in 1 file
sectionembedding
Variable F : {set 'I_N}.
definition sparse_emb source, line 472
Type
forall {R : realType} [N : nat] [F : {set 'I_N}], 'cV_#|F| -> 'rV_N
Definition
Definition sparse_emb (w : 'cV[R]_#|F|) : 'rV[R]_N :=
  \sum_j w j 0 *: delta_mx 0 (enum_val j).

The coordinates of F, in the order of enum_val.

Used by 10 declarations in 1 file
definition sparse_proj source, line 474
Type
forall {R : realType} [N : nat] (F : {set 'I_N}), 'rV_N -> 'cV_#|F|
Definition
Definition sparse_proj (z : 'rV[R]_N) : 'cV[R]_#|F| := \col_j z 0 (enum_val j).
Used by 5 declarations in 1 file
lemma sparse_embE source, line 476 
forall {R : realType} [N : nat] [F : {set 'I_N}] (w : 'cV_#|F|) (i : 'I_N),
sparse_emb w 0 i = \sum_j w j 0 * (enum_val j == i)%:R
Statement as written in the source
Lemma sparse_embE w i :
  sparse_emb w 0 i = \sum_j w j 0 * (enum_val j == i)%:R.
Used by 4 declarations in 1 file
lemma sparse_emb_val source, line 483 
forall {R : realType} [N : nat] [F : {set 'I_N}] (w : 'cV_#|F|) (j : 'I_#|[eta F]|),
sparse_emb w 0 (enum_val j) = w j 0
Statement as written in the source
Lemma sparse_emb_val w j : sparse_emb w 0 (enum_val j) = w j 0.
Used by 2 declarations in 1 file
lemma sparse_emb_out source, line 489 
forall {R : realType} [N : nat] [F : {set 'I_N}] (w : 'cV_#|F|) [i : 'I_N],
i \notin F -> sparse_emb w 0 i = 0
Statement as written in the source
Lemma sparse_emb_out w i : i \notin F -> sparse_emb w 0 i = 0.
Used by 2 declarations in 1 file
lemma sparse_emb_dot source, line 496 
forall {R : realType} [N : nat] [F : {set 'I_N}] (w w' : 'cV_#|F|),
mxdot (sparse_emb w) (sparse_emb w') = mxdot w w'
Statement as written in the source
Lemma sparse_emb_dot w w' : mxdot (sparse_emb w) (sparse_emb w') = mxdot w w'.
Used by 3 declarations in 1 file
lemma sparse_emb_proj source, line 507 
forall {R : realType} [N : nat] [F : {set 'I_N}] [z : 'rV_N],
supp z \subset F -> sparse_emb (sparse_proj F z) = z
Statement as written in the source
Lemma sparse_emb_proj z : supp z \subset F -> sparse_emb (sparse_proj z) = z.
Used by 3 declarations in 1 file
lemma sparse_embB source, line 523 
forall {R : realType} [N : nat] [F : {set 'I_N}]
  (w w' : 'cV[R]_#|F|),
sparse_emb (w - w') = sparse_emb w - sparse_emb w'
Statement as written in the source
Lemma sparse_embB w w' : sparse_emb (w - w') = sparse_emb w - sparse_emb w'.
Used by 1 declaration in 1 file
lemma sparse_proj_dot source, line 529 
forall {R : realType} [N : nat] [F : {set 'I_N}] [z : 'rV_N],
supp z \subset F -> mxdot (sparse_proj F z) (sparse_proj F z) = mxdot z z
Statement as written in the source
Lemma sparse_proj_dot z : supp z \subset F ->
  mxdot (sparse_proj z) (sparse_proj z) = mxdot z z.
Used by 2 declarations in 1 file
lemma sparse_net main result source, line 534 
forall {R : realType} [N : nat] (F : {set 'I_N}) [al eps : R],
0 <= al ->
0 < eps ->
exists S0 : seq 'rV_N,
  [/\ forall y : 'rV[R]_N, y \in S0 -> sball F al y,
      forall z : 'rV_N,
      sball F al z ->
      exists2 y : 'rV[R]_N,
        y \in S0 & mxdot (z - y) (z - y) <= eps ^+ 2
    & (size S0)%:R <= (2 * expR 1 * (1 + 2 / eps)) ^+ #|F|]

A net of the sparse vectors supported in F, of size exponential in |F|.

Main result

Stated in the README together with gram_off_decouple.

Statement as written in the source
Lemma sparse_net (al eps : R) : 0 <= al -> 0 < eps ->
  exists S : seq 'rV[R]_N, [/\ forall y, y \in S -> sball F al y,
    forall z, sball F al z ->
      exists2 y, y \in S & mxdot (z - y) (z - y) <= eps ^+ 2 &
    (size S)%:R <= (2 * expR 1 * (1 + 2 / eps)) ^+ #|F|].
Used by 1 declaration in 1 file
sectioncounting
Context {R : realType}.
lemma card_small_sets source, line 574 
forall N s : nat, #|[set F | (#|F| <= s)%N]%SET| = (\sum_(j < s.+1) 'C(N, j))%N
Statement as written in the source
Lemma card_small_sets N s :
  #|[set F : {set 'I_N} | (#|F| <= s)%N]%SET| = (\sum_(j < s.+1) 'C(N, j))%N.
Used by 2 declarations in 1 file
lemma small_sets_le main result source, line 594 
forall {R : realType} [N s : nat],
(0 < s)%N ->
(s <= N)%N -> (#|[set F | (#|F| <= s)%N]%SET|%:R : R) <= ((expR 1 * N%:R / s%:R) ^+ s : R)

There are at most (e N / s)^s subsets of size at most s.

Main result

Stated in the README together with gram_off_decouple.

Statement as written in the source
Lemma small_sets_le N s : (0 < s)%N -> (s <= N)%N ->
  (#|[set F : {set 'I_N} | (#|F| <= s)%N]%SET|)%:R <=
  (expR 1 * N%:R / s%:R) ^+ s :> R.
Used by 2 declarations in 1 file
sectiongram_off_props
Context {R : realType} (N n : nat) (x : N.-tuple 'rV[R]_n).
Implicit Types (u v w : 'rV[R]_N).
lemma gram_offC source, line 635 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (u v : 'rV_N),
gram_off x u v = gram_off x v u
Statement as written in the source
Lemma gram_offC u v : gram_off x u v = gram_off x v u.
Used by 4 declarations in 1 file
lemma gram_offDl source, line 641 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (u v w : 'rV_N),
gram_off x (u + v) w = gram_off x u w + gram_off x v w
Statement as written in the source
Lemma gram_offDl u v w : gram_off x (u + v) w = gram_off x u w + gram_off x v w.
Used by 4 declarations in 1 file
lemma gram_offZl source, line 650 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (a : R) (u w : 'rV_N),
gram_off x (a *: u) w = a * gram_off x u w
Statement as written in the source
Lemma gram_offZl a u w : gram_off x (a *: u) w = a * gram_off x u w.
Used by 2 declarations in 1 file
lemma gram_off0l source, line 656 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (w : 'rV_N), gram_off x 0 w = 0
Statement as written in the source
Lemma gram_off0l w : gram_off x 0 w = 0.
Used by 3 declarations in 1 file
lemma gram_off_suml source, line 659 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) [I : Type] 
  (r : seq I) (P : pred I) (F : I -> 'rV_N) (w : 'rV_N),
gram_off x (\sum_(i <- r | P i) F i) w = \sum_(i <- r | P i) gram_off x (F i) w
Statement as written in the source
Lemma gram_off_suml (I : Type) (r : seq I) (P : pred I)
    (F : I -> 'rV[R]_N) w :
  gram_off x (\sum_(i <- r | P i) F i) w =
  \sum_(i <- r | P i) gram_off x (F i) w.
Used by 1 declaration in 1 file
lemma gram_offDr source, line 668 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (u v w : 'rV_N),
gram_off x u (v + w) = gram_off x u v + gram_off x u w
Statement as written in the source
Lemma gram_offDr u v w : gram_off x u (v + w) = gram_off x u v + gram_off x u w.
Used by 2 declarations in 1 file
lemma gram_off_sumr source, line 671 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) [I : Type] 
  (r : seq I) (P : pred I) (F : I -> 'rV_N) (u : 'rV_N),
gram_off x u (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) gram_off x u (F i)
Statement as written in the source
Lemma gram_off_sumr (I : Type) (r : seq I) (P : pred I)
    (F : I -> 'rV[R]_N) u :
  gram_off x u (\sum_(i <- r | P i) F i) =
  \sum_(i <- r | P i) gram_off x u (F i).
lemma diag_part_le source, line 680 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (u v : 'rV_N),
`|\sum_i u 0 i * v 0 i * mxdot (tnth x i) (tnth x i)| <=
maxnorm x ^+ 2 * (frobenius u * frobenius v)

The diagonal part is bounded by the largest squared norm of the x_i.

Statement as written in the source
Lemma diag_part_le u v :
  `|\sum_i u 0 i * v 0 i * mxdot (tnth x i) (tnth x i)| <=
  maxnorm x ^+ 2 * (frobenius u * frobenius v).
Used by 2 declarations in 1 file
sectionrip_constant
Context {R : realType} (N n m : nat) (x : N.-tuple 'rV[R]_n).
definition sparse_ball source, line 709
Type
forall {R : realType} [N : nat], nat -> set 'rV_N
Definition
Definition sparse_ball : set 'rV[R]_N :=
  [set u | (#|supp u| <= m)%N /\ mxdot u u <= 1].

The m-sparse vectors of the unit ball.

Used by 4 declarations in 1 file
definition rip_const main result source, line 714
Type
forall {R : realType} [N n : nat], nat -> N.-tuple 'rV_n -> R
Definition
Definition rip_const : R := sup [set `|gram_off x u u| | u in sparse_ball].

B_m^2 of Adamczak, Litvak, Pajor and Tomczak-Jaegermann: the largest off-diagonal part of |sum_i u_i x_i|^2 over the m-sparse unit vectors.

Main result

Stated in the README together with restricted_isometry.

Used by 9 declarations in 1 file
lemma has_sup_rip source, line 716 
forall {R : realType} [N n : nat] (m : nat) (x : N.-tuple 'rV_n),
has_sup [set `|gram_off x u u| | u in sparse_ball m]
Statement as written in the source
Lemma has_sup_rip : has_sup [set `|gram_off x u u| | u in sparse_ball].
Used by 3 declarations in 1 file
lemma rip_const_ge0 source, line 732 
forall {R : realType} [N n : nat] (m : nat) (x : N.-tuple 'rV_n), 0 <= rip_const m x
Statement as written in the source
Lemma rip_const_ge0 : 0 <= rip_const.
Used by 4 declarations in 1 file
lemma supp_scale source, line 739 
forall {R : realType} [N : nat] [a : R] (u : 'rV_N), a != 0 -> supp (a *: u) = supp u
Statement as written in the source
Lemma supp_scale (a : R) (u : 'rV[R]_N) : a != 0 -> supp (a *: u) = supp u.
Used by 1 declaration in 1 file
lemma gram_off_rip main result source, line 743 
forall {R : realType} [N n m : nat] (x : N.-tuple 'rV_n) [u : 'rV_N],
(#|supp u| <= m)%N -> `|gram_off x u u| <= rip_const m x * mxdot u u

Homogeneity: |gram_off x u u| <= B_m^2 |u|^2 for every m-sparse u.

Main result, as the README states it

With B^2 = rip_const m x (the supremum above) and C = max_i |x_i|, for all m-sparse u and v: |gram_off x u u| <= B^2 |u|^2, |sum_i u_i x_i| <= sqrt (B^2 + C^2) |u| and |gram_off x u v| <= (B^2 + 2 C^2) |u| |v|, where gram_off x u v = sum_(i <> j) u_i v_j <x_i, x_j>.

Statement as written in the source
Lemma gram_off_rip (u : 'rV[R]_N) : (#|supp u| <= m)%N ->
  `|gram_off x u u| <= rip_const * mxdot u u.
Used by 2 declarations in 1 file
lemma tuple_mx_rip main result source, line 765 
forall {R : realType} [N n m : nat] (x : N.-tuple 'rV_n) [u : 'rV_N],
(#|supp u| <= m)%N ->
frobenius (u *m tuple_mx x) <=
Num.ExtraDef.sqrtr (rip_const m x + maxnorm x ^+ 2) * frobenius u
Main result

Stated in the README together with gram_off_rip.

Statement as written in the source
Lemma tuple_mx_rip (u : 'rV[R]_N) : (#|supp u| <= m)%N ->
  frobenius (u *m tuple_mx x) <=
  Num.sqrt (rip_const + maxnorm x ^+ 2) * frobenius u.
Used by 2 declarations in 1 file
lemma gram_off_rip2 main result source, line 784 
forall {R : realType} [N n m : nat] (x : N.-tuple 'rV_n) [u v : 'rV_N],
(#|supp u| <= m)%N ->
(#|supp v| <= m)%N ->
`|gram_off x u v| <= (rip_const m x + 2 * maxnorm x ^+ 2) * (frobenius u * frobenius v)
Main result

Stated in the README together with gram_off_rip.

Statement as written in the source
Lemma gram_off_rip2 (u v : 'rV[R]_N) :
  (#|supp u| <= m)%N -> (#|supp v| <= m)%N ->
  `|gram_off x u v| <=
  (rip_const + 2 * maxnorm x ^+ 2) * (frobenius u * frobenius v).
Used by 1 declaration in 1 file
sectionlevels
Context {R : realType} (N m : nat).
Implicit Types (z : 'rV[R]_N).
definition lvl_lo source, line 813
Type
forall {R : realType}, nat -> R
Definition
Definition lvl_lo (k : nat) : R := if k is k'.+1 then 4 ^+ k' else 0.

Level k of z collects the coordinates with 4^(k-1) < m z_i^2 <= 4^k (0 < m z_i^2 <= 1 for k = 0): it has at most lsize k elements, each at most alpha k = 2^k / sqrt m in absolute value.

Used by 3 declarations in 1 file
definition level source, line 815
Type
forall {R : realType} [N : nat], nat -> 'rV_N -> nat -> {set 'I_N}
Definition
Definition level z k : {set 'I_N} :=
  [set i | lvl_lo k < m%:R * z 0 i ^+ 2 <= 4 ^+ k].
Used by 7 declarations in 1 file
definition lsize source, line 818
Type
nat -> nat -> nat
Definition
Definition lsize k : nat := if k is k'.+1 then (m %/ 4 ^ k')%N else m.
Used by 16 declarations in 1 file
definition alpha source, line 820
Type
forall {R : realType}, nat -> nat -> R
Definition
Definition alpha k : R := 2 ^+ k / Num.sqrt m%:R.
Used by 10 declarations in 1 file
lemma lvl_lo_ge0 source, line 822 
forall {R : realType} (k : nat), 0 <= lvl_lo k
Statement as written in the source
Lemma lvl_lo_ge0 k : 0 <= lvl_lo k.
Used by 1 declaration in 1 file
lemma level_supp source, line 825 
forall {R : realType} [N : nat] (m : nat) (z : 'rV_N) (k : nat), level m z k \subset supp z
Statement as written in the source
Lemma level_supp z k : level z k \subset supp z.
Used by 2 declarations in 1 file
lemma level_uniq source, line 832 
forall {R : realType} [N m : nat] [z : 'rV_N] [k k' : nat] [i : 'I_N],
i \in level m z k -> i \in level m z k' -> k = k'
Statement as written in the source
Lemma level_uniq z k k' i : i \in level z k -> i \in level z k' -> k = k'.
Used by 2 declarations in 1 file
lemma level_cover source, line 845 
forall {R : realType} [N m : nat] [z : 'rV_N] [l : nat],
(0 < m)%N ->
mxdot z z <= 1 ->
(m <= 4 ^ l)%N ->
forall [i : 'I_N], z 0 i != 0 -> exists2 k : nat, (k <= l)%N & i \in level m z k
Statement as written in the source
Lemma level_cover z l : (0 < m)%N -> mxdot z z <= 1 -> (m <= 4 ^ l)%N ->
  forall i, z 0 i != 0 -> exists2 k, (k <= l)%N & i \in level z k.
Used by 1 declaration in 1 file
lemma level_size source, line 865 
forall {R : realType} [N m : nat] [z : 'rV_N] (k : nat),
(#|supp z| <= m)%N -> mxdot z z <= 1 -> (#|level m z k| <= lsize m k)%N
Statement as written in the source
Lemma level_size z k : (#|supp z| <= m)%N -> mxdot z z <= 1 ->
  (#|level z k| <= lsize k)%N.
Used by 1 declaration in 1 file
lemma level_alpha source, line 884 
forall {R : realType} [N m : nat] [z : 'rV_N] [k : nat] [i : 'I_N],
(0 < m)%N -> i \in level m z k -> `|z 0 i| <= alpha m k
Statement as written in the source
Lemma level_alpha z k i : (0 < m)%N -> i \in level z k -> `|z 0 i| <= alpha k.
Used by 1 declaration in 1 file
lemma level_sum source, line 896 
forall {R : realType} [N m : nat] [z : 'rV_N] [l : nat],
(0 < m)%N -> mxdot z z <= 1 -> (m <= 4 ^ l)%N -> z = \sum_(k < l.+1) restr (level m z k) z
Statement as written in the source
Lemma level_sum z l : (0 < m)%N -> mxdot z z <= 1 -> (m <= 4 ^ l)%N ->
  z = \sum_(k < l.+1) restr (level z k) z.
Used by 1 declaration in 1 file
sectionsupports
Context {R : realType} (N : nat).
Implicit Types (u v : 'rV[R]_N) (S : {set 'I_N}).
definition supported source, line 916
Type
forall {R : realType} [N : nat], {set 'I_N} -> 'rV_N -> Prop
Definition
Definition supported S u := forall i, i \notin S -> u 0 i = 0.

u vanishes outside S.

Used by 9 declarations in 1 file
lemma supportedP source, line 918 
forall {R : realType} [N : nat] (S0 : {set 'I_N}) (u : 'rV_N),
supported S0 u <-> supp u \subset S0
Statement as written in the source
Lemma supportedP S u : supported S u <-> supp u \subset S.
Used by 3 declarations in 1 file
lemma supported_sum source, line 926 
forall {R : realType} [N : nat] [I : Type] (r : seq I) [P : pred I] 
  [F : I -> 'rV_N] [S0 : {set 'I_N}],
(forall i : I, P i -> supported S0 (F i)) -> supported S0 (\sum_(i <- r | P i) F i)
Statement as written in the source
Lemma supported_sum (I : Type) (r : seq I) (P : pred I) (F : I -> 'rV[R]_N) S :
  (forall i, P i -> supported S (F i)) -> supported S (\sum_(i <- r | P i) F i).
Used by 1 declaration in 1 file
lemma supportedB source, line 933 
forall {R : realType} [N : nat] [S0 : {set 'I_N}] [u v : 'rV_N],
supported S0 u -> supported S0 v -> supported S0 (u - v)
Statement as written in the source
Lemma supportedB S u v : supported S u -> supported S v -> supported S (u - v).
Used by 1 declaration in 1 file
lemma supported_restr source, line 936 
forall {R : realType} [N : nat] [S0 : {set 'I_N}] (E : {set 'I_N}) [u : 'rV_N],
supported S0 u -> supported S0 (restr E u)
Statement as written in the source
Lemma supported_restr S E u : supported S u -> supported S (restr E u).
Used by 1 declaration in 1 file
lemma supported_restrE source, line 939 
forall {R : realType} [N : nat] [E : {set 'I_N}] (u : 'rV_N), supported E (restr E u)
Statement as written in the source
Lemma supported_restrE E u : supported E (restr E u).
Used by 1 declaration in 1 file
lemma supported_sub source, line 942 
forall {R : realType} [N : nat] [S0 S' : {set 'I_N}] [u : 'rV_N],
S0 \subset S' -> supported S0 u -> supported S' u
Statement as written in the source
Lemma supported_sub S S' u : S \subset S' -> supported S u -> supported S' u.
Used by 1 declaration in 1 file
lemma supported_card source, line 948 
forall {R : realType} [N : nat] [S0 : {set 'I_N}] [u : 'rV_N] [m : nat],
supported S0 u -> (#|S0| <= m)%N -> (#|supp u| <= m)%N
Statement as written in the source
Lemma supported_card S u (m : nat) : supported S u -> (#|S| <= m)%N ->
  (#|supp u| <= m)%N.
Used by 1 declaration in 1 file
lemma disj_supported source, line 954 
forall {R : realType} [N : nat] [S0 S' : {set 'I_N}] [u v : 'rV_N],
supported S0 u ->
supported S' v -> (forall i : 'I_N, i \in S0 -> i \in S' -> False) -> disj u v
Statement as written in the source
Lemma disj_supported S S' u v : supported S u -> supported S' v ->
  (forall i, i \in S -> i \in S' -> False) -> disj u v.
Used by 1 declaration in 1 file
lemma mxdot_disj source, line 961 
forall {R : realType} [N : nat] [u v : 'rV_N], disj u v -> mxdot u v = 0
Statement as written in the source
Lemma mxdot_disj u v : disj u v -> mxdot u v = 0.
Used by 1 declaration in 1 file
lemma mxdot_restr source, line 967 
forall {R : realType} [N : nat] (E : {set 'I_N}) (u : 'rV_N),
mxdot (restr E u) (restr E u) <= mxdot u u
Statement as written in the source
Lemma mxdot_restr E u : mxdot (restr E u) (restr E u) <= mxdot u u.
Used by 2 declarations in 1 file
lemma mxdot_sum_disj source, line 974 
forall {R : realType} [N : nat] [I : eqType] [r : seq I] [F : I -> 'rV_N],
uniq r ->
(forall i j : I, i != j -> disj (F i) (F j)) ->
mxdot (\sum_(i <- r) F i) (\sum_(i <- r) F i) = \sum_(i <- r) mxdot (F i) (F i)

Pythagoras for vectors with pairwise disjoint supports.

Statement as written in the source
Lemma mxdot_sum_disj (I : eqType) (r : seq I) (F : I -> 'rV[R]_N) : uniq r ->
  (forall i j, i != j -> disj (F i) (F j)) ->
  mxdot (\sum_(i <- r) F i) (\sum_(i <- r) F i) =
  \sum_(i <- r) mxdot (F i) (F i).
Used by 2 declarations in 1 file
sectiontriangular
Context {R : realType} (N n : nat) (x : N.-tuple 'rV[R]_n).
lemma gram_off_tri source, line 998 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (a : nat -> 'rV_N) [k L : nat],
(k <= L)%N ->
gram_off x (\sum_(k <= r < L) a r) (\sum_(k <= r < L) a r) =
\sum_(k <= j < L)
   (gram_off x (a j) (a j) + 2 * gram_off x (a j) (\sum_(j.+1 <= r < L) a r))

The form of a sum: the diagonal terms and twice the terms of each vector against the sum of the later ones.

Statement as written in the source
Lemma gram_off_tri (a : nat -> 'rV[R]_N) k L : (k <= L)%N ->
  gram_off x (\sum_(k <= r < L) a r) (\sum_(k <= r < L) a r) =
  \sum_(k <= j < L) (gram_off x (a j) (a j) +
    2 * gram_off x (a j) (\sum_(j.+1 <= r < L) a r)).
Used by 1 declaration in 1 file
sectiondeterministic
Context {R : realType} (N n m l : nat) (x : N.-tuple 'rV[R]_n).
Hypotheses (m0 : (0 < m)%N) (ml : (m <= 4 ^ l)%N).
Variables (eps t : nat -> R) (beta : R).
Variable nt : nat -> {set 'I_N} -> seq 'rV[R]_N.

nt k F is a net of mesh eps k of the vectors supported in F of norm at most 1 and coordinates at most alpha k.

Hypothesis ntP : forall k F y, y \in nt k F -> sball F (alpha m k) y.
Hypothesis ntN : forall k F z, sball F (alpha m k) z ->
  exists2 y, y \in nt k F & mxdot (z - y) (z - y) <= eps k ^+ 2.
Hypothesis eps_sum : \sum_(0 <= k < l.+1) eps k ^+ 2 <= beta ^+ 2 / 9.
Hypotheses (beta0 : 0 <= beta) (beta1 : beta <= 1 / 2).
Hypothesis t0 : forall k, 0 <= t k.
definition upper source, line 1031
Type
forall {R : realType} [N : nat],
nat -> nat -> (nat -> {set 'I_N} -> seq 'rV_N) -> nat -> 'rV_N -> Prop
Definition
Definition upper (k : nat) (v : 'rV[R]_N) := exists yr : nat -> 'rV[R]_N,
  (forall r, (k < r <= l)%N ->
    exists2 F : {set 'I_N}, (#|F| <= lsize m r)%N & yr r \in nt r F) /\
  v = \sum_(k.+1 <= r < l.+1) yr r.

The sums of net points of the levels above k.

Used by 2 declarations in 1 file

The complement of the bad events of the union bound.

Hypothesis goodW : forall k (F E : {set 'I_N}) y, (k <= l)%N ->
  (#|F| <= lsize m k)%N -> E \subset F -> y \in nt k F ->
  `|mxdot (restr E y *m tuple_mx x) (restr (F :\: E) y *m tuple_mx x)| <=
  t k * frobenius (restr (F :\: E) y *m tuple_mx x).
Hypothesis goodX : forall k (F : {set 'I_N}) y v, (k <= l)%N ->
  (#|F| <= lsize m k)%N -> y \in nt k F -> upper k v ->
  `|mxdot (y *m tuple_mx x) (restr (~: F) v *m tuple_mx x)| <=
  t k * frobenius (restr (~: F) v *m tuple_mx x).
lemma gram_off_ball source, line 1046 
forall {R : realType} [N n m l : nat] [x : N.-tuple 'rV_n],
(0 < m)%N ->
(m <= 4 ^ l)%N ->
forall [eps t : nat -> R] [beta : R] [nt : nat -> {set 'I_N} -> seq 'rV_N],
(forall (k : nat) (F : {set 'I_N}) (y : 'rV[R]_N),
 y \in nt k F -> sball F (alpha m k) y) ->
(forall (k : nat) (F : {set 'I_N}) (z : 'rV_N),
 sball F (alpha m k) z ->
 exists2 y : 'rV[R]_N,
   y \in nt k F & mxdot (z - y) (z - y) <= eps k ^+ 2) ->
\sum_(0 <= k < l.+1) eps k ^+ 2 <= beta ^+ 2 / 9 ->
0 <= beta ->
beta <= 1 / 2 ->
(forall k : nat, 0 <= t k) ->
(forall (k : nat) (F E : {set 'I_N}) (y : 'rV[R]_N),
 (k <= l)%N ->
 (#|F| <= lsize m k)%N ->
 E \subset F ->
 y \in nt k F ->
 `|mxdot (restr E y *m tuple_mx x) (restr (F :\: E) y *m tuple_mx x)| <=
 t k * frobenius (restr (F :\: E) y *m tuple_mx x)) ->
(forall (k : nat) (F : {set 'I_N}) (y : 'rV[R]_N)
   (v : 'rV_N),
 (k <= l)%N ->
 (#|F| <= lsize m k)%N ->
 y \in nt k F ->
 upper m l nt k v ->
 `|mxdot (y *m tuple_mx x) (restr (~: F) v *m tuple_mx x)| <=
 t k * frobenius (restr (~: F) v *m tuple_mx x)) ->
forall [z : 'rV_N],
sparse_ball m z ->
`|gram_off x z z| <=
8 * (\sum_(0 <= k < l.+1) t k) * Num.ExtraDef.sqrtr (rip_const m x + maxnorm x ^+ 2) +
beta * (rip_const m x + 2 * maxnorm x ^+ 2)
Statement as written in the source
Lemma gram_off_ball z : sparse_ball m z ->
  `|gram_off x z z| <=
  8 * (\sum_(0 <= k < l.+1) t k) * Num.sqrt (rip_const m x + maxnorm x ^+ 2) +
  beta * (rip_const m x + 2 * maxnorm x ^+ 2).
Used by 1 declaration in 1 file
theorem rip_const_le source, line 1198 
forall {R : realType} [N n m l : nat] [x : N.-tuple 'rV_n],
(0 < m)%N ->
(m <= 4 ^ l)%N ->
forall [eps t : nat -> R] [beta : R] [nt : nat -> {set 'I_N} -> seq 'rV_N],
(forall (k : nat) (F : {set 'I_N}) (y : 'rV[R]_N),
 y \in nt k F -> sball F (alpha m k) y) ->
(forall (k : nat) (F : {set 'I_N}) (z : 'rV_N),
 sball F (alpha m k) z ->
 exists2 y : 'rV[R]_N,
   y \in nt k F & mxdot (z - y) (z - y) <= eps k ^+ 2) ->
\sum_(0 <= k < l.+1) eps k ^+ 2 <= beta ^+ 2 / 9 ->
0 <= beta ->
beta <= 1 / 2 ->
(forall k : nat, 0 <= t k) ->
(forall (k : nat) (F E : {set 'I_N}) (y : 'rV[R]_N),
 (k <= l)%N ->
 (#|F| <= lsize m k)%N ->
 E \subset F ->
 y \in nt k F ->
 `|mxdot (restr E y *m tuple_mx x) (restr (F :\: E) y *m tuple_mx x)| <=
 t k * frobenius (restr (F :\: E) y *m tuple_mx x)) ->
(forall (k : nat) (F : {set 'I_N}) (y : 'rV[R]_N)
   (v : 'rV_N),
 (k <= l)%N ->
 (#|F| <= lsize m k)%N ->
 y \in nt k F ->
 upper m l nt k v ->
 `|mxdot (y *m tuple_mx x) (restr (~: F) v *m tuple_mx x)| <=
 t k * frobenius (restr (~: F) v *m tuple_mx x)) ->
rip_const m x <=
256 * (\sum_(0 <= k < l.+1) t k) ^+ 2 + 32 * (\sum_(0 <= k < l.+1) t k) * maxnorm x +
8 * beta * maxnorm x ^+ 2
Statement as written in the source
Theorem rip_const_le : rip_const m x <=
  256 * (\sum_(0 <= k < l.+1) t k) ^+ 2 +
  32 * (\sum_(0 <= k < l.+1) t k) * maxnorm x + 8 * beta * maxnorm x ^+ 2.
Used by 1 declaration in 1 file
lemma measure_bigsetU_le source, line 1230 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  (mu : measure T R) [I : Type] (r : seq I) [F : I -> set T],
(forall i : I, d.-measurable (F i)) ->
(mu (\big[setU/set0]_(i <- r) F i) <= (\sum_(i <- r) mu (F i))%R)%E
Statement as written in the source
Lemma measure_bigsetU_le d (T : measurableType d) (R : realType)
    (mu : {measure set T -> \bar R}) (I : Type) (r : seq I) (F : I -> set T) :
  (forall i, measurable (F i)) ->
  (mu (\big[setU/set0]_(i <- r) F i) <= \sum_(i <- r) mu (F i))%E.
Used by 2 declarations in 1 file
sectionnumeric
Context {R : realType}.
lemma ln_le_sub1 source, line 1244 
forall {R : realType} [x : R], 0 < x -> ln x <= x - 1
Statement as written in the source
Lemma ln_le_sub1 (x : R) : 0 < x -> ln x <= x - 1.
Used by 2 declarations in 1 file
lemma ln2_le1 source, line 1251 
forall {R : realType}, ln (2 : R) <= 1
Statement as written in the source
Lemma ln2_le1 : ln (2 : R) <= 1.
Used by 3 declarations in 1 file
lemma lnX_le source, line 1256 
forall {R : realType} [x : R] (k : nat), 0 < x -> ln (x ^+ k) = k%:R * ln x
Statement as written in the source
Lemma lnX_le (x : R) (k : nat) : 0 < x -> ln (x ^+ k) = k%:R * ln x.
Used by 2 declarations in 1 file
lemma slog_le source, line 1260 
forall {R : realType} [s sigma : R], 0 < s -> s <= sigma -> s * ln (sigma / s) <= sigma

s ln (sigma / s) <= sigma.

Statement as written in the source
Lemma slog_le (s sigma : R) : 0 < s -> s <= sigma ->
  s * ln (sigma / s) <= sigma.
Used by 1 declaration in 1 file
sectionconfigurations
Context {R : realType} (N m l : nat) (beta : R).
Hypotheses (m0 : (0 < m)%N) (beta0 : 0 < beta).
definition mesh source, line 1278
Type
forall {R : realType}, R -> nat -> R
Definition
Definition mesh k : R := beta / 2 ^+ k.+2.

The mesh of the net of level k.

Used by 7 declarations in 1 file
lemma mesh_gt0 source, line 1280 
forall {R : realType} [beta : R], 0 < beta -> forall k : nat, 0 < mesh beta k
Statement as written in the source
Lemma mesh_gt0 k : 0 < mesh k.
Used by 3 declarations in 1 file
lemma alpha_ge0 source, line 1283 
forall {R : realType} (m k : nat), (0 : R) <= (alpha m k : R)
Statement as written in the source
Lemma alpha_ge0 k : 0 <= alpha m k :> R.
Used by 2 declarations in 1 file
definition net_spec source, line 1286
Type
forall {R : realType} [N : nat], nat -> R -> nat -> {set 'I_N} -> seq 'rV_N -> Prop
Definition
Definition net_spec k (F : {set 'I_N}) (S : seq 'rV[R]_N) :=
  [/\ forall y, y \in S -> sball F (alpha m k) y,
    forall z, sball F (alpha m k) z ->
      exists2 y, y \in S & mxdot (z - y) (z - y) <= mesh k ^+ 2 &
    (size S)%:R <= (2 * expR 1 * (1 + 2 / mesh k)) ^+ #|F|].
Used by 2 declarations in 1 file
definition net source, line 1293
Type
forall {R : realType} [N : nat], nat -> R -> nat -> {set 'I_N} -> seq 'rV_N
Definition
Definition net k F : seq 'rV[R]_N := xget [::] (net_spec k F).

A net of level k for the vectors supported in F.

Used by 11 declarations in 1 file
lemma netP source, line 1295 
forall {R : realType} [N : nat] (m : nat) [beta : R],
0 < beta -> forall (k : nat) (F : {set 'I_N}), net_spec m beta k F (net m beta k F)
Statement as written in the source
Lemma netP k F : net_spec k F (net k F).
Used by 3 declarations in 1 file
definition sets_le source, line 1301
Type
forall N : nat, nat -> seq {set 'I_N}
Definition
Definition sets_le s : seq {set 'I_N} :=
  enum [set F : {set 'I_N} | (#|F| <= s)%N]%SET.
Used by 8 declarations in 1 file
definition wconf source, line 1305
Type
forall {R : realType} (N : nat), nat -> R -> nat -> seq ('rV_N * 'rV_N)
Definition
Definition wconf k : seq ('rV[R]_N * 'rV[R]_N) :=
  flatten [seq flatten [seq [seq (restr E y, restr (F :\: E) y) | y <- net k F]
    | E <- enum (powerset F)] | F <- sets_le (lsize m k)].

The pairs of the decoupled diagonal terms of level k.

Used by 5 declarations in 1 file
definition allnet source, line 1309
Type
forall {R : realType} (N : nat), nat -> R -> nat -> seq 'rV_N
Definition
Definition allnet r : seq 'rV[R]_N :=
  flatten [seq net r F | F <- sets_le (lsize m r)].
Used by 3 declarations in 1 file
fixpoint vlist source, line 1313
Type
forall {R : realType} (N : nat), nat -> nat -> R -> nat -> seq 'rV_N
Definition
Fixpoint vlist d : seq 'rV[R]_N :=
  if d is d'.+1 then [seq y + v | y <- allnet (l - d'), v <- vlist d']
  else [:: 0].

The sums of net points of the levels l - d + 1, ..., l.

Used by 4 declarations in 1 file
definition xconf source, line 1318
Type
forall {R : realType} (N : nat), nat -> nat -> R -> nat -> seq ('rV_N * 'rV_N)
Definition
Definition xconf k : seq ('rV[R]_N * 'rV[R]_N) :=
  flatten [seq flatten [seq [seq (y, restr (~: F) v) | v <- vlist (l - k)]
    | y <- net k F] | F <- sets_le (lsize m k)].

The pairs of the terms of level k against the levels above.

Used by 5 declarations in 1 file
lemma mem_sets_le source, line 1322 
forall [N : nat] (s : nat) (F : {set 'I_N}),
(F \in sets_le N s) = (#|F| <= s)%N
Statement as written in the source
Lemma mem_sets_le s F : (F \in sets_le s) = (#|F| <= s)%N.
Used by 7 declarations in 1 file
lemma mem_wconf source, line 1325 
forall {R : realType} [N m : nat] [beta : R] [k : nat] [F E : {set 'I_N}]
  [y : 'rV[R]_N],
(#|F| <= lsize m k)%N ->
E \subset F -> y \in net m beta k F -> (restr E y, restr (F :\: E) y) \in wconf N m beta k
Statement as written in the source
Lemma mem_wconf k (F E : {set 'I_N}) y : (#|F| <= lsize m k)%N ->
  E \subset F -> y \in net k F -> (restr E y, restr (F :\: E) y) \in wconf k.
Used by 1 declaration in 1 file
lemma mem_xconf source, line 1337 
forall {R : realType} [N m l : nat] [beta : R] [k : nat] [F : {set 'I_N}]
  [y v : 'rV[R]_N],
(#|F| <= lsize m k)%N ->
y \in net m beta k F ->
v \in vlist N m l beta (l - k) -> (y, restr (~: F) v) \in xconf N m l beta k
Statement as written in the source
Lemma mem_xconf k (F : {set 'I_N}) y v : (#|F| <= lsize m k)%N ->
  y \in net k F -> v \in vlist (l - k) -> (y, restr (~: F) v) \in xconf k.
Used by 1 declaration in 1 file
lemma mem_allnet source, line 1349 
forall {R : realType} [N m : nat] [beta : R] [r : nat] [F : {set 'I_N}]
  [y : 'rV[R]_N],
(#|F| <= lsize m r)%N -> y \in net m beta r F -> y \in allnet N m beta r
Statement as written in the source
Lemma mem_allnet r (F : {set 'I_N}) y : (#|F| <= lsize m r)%N ->
  y \in net r F -> y \in allnet r.
Used by 1 declaration in 1 file
lemma upper_vlist source, line 1357 
forall {R : realType} [N m l : nat] [beta : R] [k : nat] [v : 'rV_N],
(k <= l)%N -> upper m l (net m beta) k v -> v \in vlist N m l beta (l - k)

Every sum of net points of the levels above k is in vlist (l - k).

Statement as written in the source
Lemma upper_vlist k v : (k <= l)%N -> upper m l net k v -> v \in vlist (l - k).
Used by 1 declaration in 1 file
definition nbase source, line 1379
Type
forall {R : realType}, R -> nat -> R
Definition
Definition nbase k : R := 2 * expR 1 * (1 + 2 / mesh k).

Sizes of the configuration lists.

Used by 9 declarations in 1 file
lemma nbase_ge1 source, line 1381 
forall {R : realType} [beta : R], 0 < beta -> forall k : nat, 1 <= nbase beta k
Statement as written in the source
Lemma nbase_ge1 k : 1 <= nbase k.
Used by 6 declarations in 1 file
lemma size_net source, line 1390 
forall {R : realType} [N : nat] (m : nat) [beta : R],
0 < beta ->
forall (k : nat) [F : {set 'I_N}] [s : nat],
(#|F| <= s)%N -> (size (net m beta k F))%:R <= nbase beta k ^+ s
Statement as written in the source
Lemma size_net k (F : {set 'I_N}) s : (#|F| <= s)%N ->
  (size (net k F))%:R <= nbase k ^+ s.
Used by 3 declarations in 1 file
definition ccount source, line 1397
Type
forall {R : realType}, nat -> nat -> R -> nat -> R
Definition
Definition ccount k : R :=
  (#|[set F : {set 'I_N} | (#|F| <= lsize m k)%N]%SET|)%:R *
  (2 * nbase k) ^+ lsize m k.
Used by 7 declarations in 1 file
lemma ccount_ge1 source, line 1401 
forall {R : realType} (N m : nat) [beta : R],
0 < beta -> forall k : nat, 1 <= ccount N m beta k
Statement as written in the source
Lemma ccount_ge1 k : 1 <= ccount k.
Used by 2 declarations in 1 file
lemma size_wconf source, line 1415 
forall {R : realType} (N m : nat) [beta : R],
0 < beta -> forall k : nat, (size (wconf N m beta k))%:R <= ccount N m beta k
Statement as written in the source
Lemma size_wconf k : (size (wconf k))%:R <= ccount k.
Used by 1 declaration in 1 file
lemma size_allnet source, line 1436 
forall {R : realType} (N m : nat) [beta : R],
0 < beta -> forall r : nat, (size (allnet N m beta r))%:R <= ccount N m beta r
Statement as written in the source
Lemma size_allnet r : (size (allnet r))%:R <= ccount r.
Used by 1 declaration in 1 file
lemma size_vlist source, line 1451 
forall {R : realType} (N m l : nat) [beta : R],
0 < beta ->
forall d : nat, (size (vlist N m l beta d))%:R <= \prod_(j < d) ccount N m beta (l - j)
Statement as written in the source
Lemma size_vlist d : (size (vlist d))%:R <= \prod_(j < d) ccount (l - j).
Used by 1 declaration in 1 file
lemma size_xconf source, line 1458 
forall {R : realType} (N m l : nat) [beta : R],
0 < beta ->
forall k : nat,
(size (xconf N m l beta k))%:R <=
ccount N m beta k * \prod_(j < l - k) ccount N m beta (l - j)
Statement as written in the source
Lemma size_xconf k :
  (size (xconf k))%:R <= ccount k * \prod_(j < l - k) ccount (l - j).
Used by 1 declaration in 1 file
lemma lnb2_le source, line 1482 
forall {R : realType} [beta : R],
0 < beta -> forall k : nat, beta <= 1 -> ln (2 * nbase beta k) <= k%:R + 7 - ln beta
Statement as written in the source
Lemma lnb2_le k : beta <= 1 -> ln (2 * nbase k) <= k%:R + 7 - ln beta.
Used by 1 declaration in 1 file
lemma ccount_le source, line 1524 
forall {R : realType} [N m : nat] [beta : R],
(0 < m)%N ->
0 < beta ->
forall k : nat,
(m <= N)%N ->
beta <= 1 ->
ccount N m beta k <= expR (4 * m%:R / 4 ^+ k * (9 + ln (N%:R / m%:R) - ln beta + 3 * k%:R))

The logarithm of the number of configurations of level k.

Statement as written in the source
Lemma ccount_le k : (m <= N)%N -> beta <= 1 ->
  ccount k <= expR (4 * m%:R / 4 ^+ k *
    (9 + ln (N%:R / m%:R) - ln beta + 3 * k%:R)).
Used by 1 declaration in 1 file
lemma mesh_sum source, line 1625 
forall {R : realType} [beta : R],
0 < beta -> forall n : nat, \sum_(0 <= k < n) mesh beta k ^+ 2 <= beta ^+ 2 / 9

The pairs of the union bound satisfy the hypotheses of cross_tail.

Statement as written in the source
Lemma mesh_sum n : \sum_(0 <= k < n) mesh k ^+ 2 <= beta ^+ 2 / 9.
Used by 1 declaration in 1 file
lemma conf_ok source, line 1640 
forall {R : realType} [N m l : nat] [beta : R],
0 < beta ->
forall [k : nat]
  [c : ('rV[R]_N * 'rV[R]_N)],
c \in wconf N m beta k ++ xconf N m l beta k ->
[/\ disj c.1 c.2, mxdot c.1 c.1 <= 1 & forall i : 'I_N, `|c.1 0 i| <= alpha m k]
Statement as written in the source
Lemma conf_ok k c : c \in wconf k ++ xconf k ->
  [/\ disj c.1 c.2, mxdot c.1 c.1 <= 1 & forall i, `|c.1 0 i| <= alpha m k].
Used by 1 declaration in 1 file
sectionunion_bound
Context {R : realType} (N n m l : nat) (mu : nat -> probability 'rV[R]_n R)
  (psi beta : R).
Hypothesis psi0 : 0 < psi.
Hypothesis sub : forall i (y : 'rV[R]_n), (i < N)%N -> mxdot y y = 1 ->
  subexponential (mu i) (fun v => mxdot v y) psi.
Hypothesis cen : forall i (y : 'rV[R]_n), (i < N)%N -> mxdot y y = 1 ->
  \int[mu i]_v mxdot v y = 0.
Hypotheses (m0 : (0 < m)%N) (ml : (m <= 4 ^ l)%N).
Hypotheses (beta0 : 0 < beta) (beta1 : beta <= 1 / 2).
Variable t : nat -> R.
Hypothesis t0 : forall k, 0 < t k.
let conf section-local source, line 1675 
Let conf k := @wconf R N m beta k ++ @xconf R N m l beta k.
Used by 3 declarations in 1 file
definition bad_event source, line 1678
Type
forall {R : realType} [N n : nat], nat -> nat -> R -> (nat -> R) -> set (N.-tuple 'rV_n)
Definition
Definition bad_event : set (N.-tuple 'rV[R]_n) :=
  \big[setU/set0]_(k < l.+1)
    \big[setU/set0]_(c <- conf k) cross_event (t k) c.1 c.2.

The union of the bad events of all levels.

Used by 4 declarations in 1 file
lemma measurable_bad_event source, line 1682 
forall {R : realType} [N n : nat] (m l : nat) (beta : R) [t : nat -> R],
(forall k : nat, 0 < t k) ->
(measure_tuple_display (measure_matrix_display default_measure_display)).-measurable
  (bad_event m l beta t)
Statement as written in the source
Lemma measurable_bad_event : measurable bad_event.
Used by 1 declaration in 1 file
lemma bad_event_le source, line 1688 
forall {R : realType} [N n : nat] (m l : nat) [mu : nat -> probability 'rV_n R]
  [psi beta : R],
0 < psi ->
(forall (i : nat) (y : 'rV_n),
 (i < N)%N -> mxdot y y = 1 -> subexponential (mu i) ((mxdot (n:=n))^~ y) psi) ->
(forall (i : nat) (y : 'rV_n), (i < N)%N -> mxdot y y = 1 -> \int[mu i]_v mxdot v y = 0) ->
0 < beta ->
forall [t : nat -> R],
(forall k : nat, 0 < t k) ->
(tuple_prod mu N (bad_event m l beta t) <=
 (\sum_(k < l.+1)
     (size ((fun k0 : nat => wconf N m beta k0 ++ xconf N m l beta k0) k))%:R *
     (2 * expR (- minr (t k ^+ 2 / (64 * psi ^+ 2)) (t k / (4 * (alpha m k * psi))))))%:E)%E
Statement as written in the source
Lemma bad_event_le : (tuple_prod mu N bad_event <=
  (\sum_(k < l.+1) (size (conf k))%:R *
    (2 * expR (- Num.min (t k ^+ 2 / (64 * psi ^+ 2))
                         (t k / (4 * (alpha m k * psi))))))%:E)%E.
Used by 1 declaration in 1 file
lemma bigsetU_mem source, line 1709 
forall [T : Type] [I : eqType] [r : seq I] [F : I -> set T] [i : I] [z : T],
i \in r -> F i z -> (\big[setU/set0]_(j <- r) F j) z
Statement as written in the source
Lemma bigsetU_mem (T : Type) (I : eqType) (r : seq I) (F : I -> set T) i z :
  i \in r -> F i z -> (\big[setU/set0]_(j <- r) F j) z.
Used by 2 declarations in 1 file
theorem rip_good source, line 1718 
forall {R : realType} [N n m l : nat] [beta : R],
(0 < m)%N ->
(m <= 4 ^ l)%N ->
0 < beta ->
beta <= 1 / 2 ->
forall [t : nat -> R],
(forall k : nat, 0 < t k) ->
forall [x : N.-tuple 'rV_n],
~ bad_event m l beta t x ->
rip_const m x <=
256 * (\sum_(0 <= k < l.+1) t k) ^+ 2 + 32 * (\sum_(0 <= k < l.+1) t k) * maxnorm x +
8 * beta * maxnorm x ^+ 2

Outside the bad event, B_m^2 is bounded by the sum T of the t k.

Statement as written in the source
Theorem rip_good x : ~ bad_event x ->
  rip_const m x <= 256 * (\sum_(0 <= k < l.+1) t k) ^+ 2 +
    32 * (\sum_(0 <= k < l.+1) t k) * maxnorm x + 8 * beta * maxnorm x ^+ 2.
Used by 1 declaration in 1 file
sectionseries
Context {R : realType}.
lemma sum_pow2 source, line 1750 
forall {R : realType} (n : nat), \sum_(k < n) (2 : R) ^+ k <= 2 ^+ n
Statement as written in the source
Lemma sum_pow2 n : \sum_(k < n) (2 : R) ^+ k <= 2 ^+ n.
Used by 1 declaration in 1 file
lemma sum_geo_lin source, line 1758 
forall {R : realType} [a : R] (n : nat),
6 <= a -> \sum_(k < n) (a + 3 * k%:R) / 2 ^+ k <= 4 * a

sum_k 2^-k (a + 3 k) <= 4 a for a >= 6

Statement as written in the source
Lemma sum_geo_lin (a : R) n : 6 <= a ->
  \sum_(k < n) (a + 3 * k%:R) / 2 ^+ k <= 4 * a.
Used by 1 declaration in 1 file
lemma sq_le_pow2 source, line 1783 
realType -> forall l : nat, (l.+1 ^ 2 <= 8 * 2 ^ l)%N
Statement as written in the source
Lemma sq_le_pow2 l : (l.+1 ^ 2 <= 8 * 2 ^ l)%N.
Used by 1 declaration in 1 file
sectionparameters
Context {R : realType} (N n m l : nat) (psi beta K : R).
Hypotheses (m0 : (0 < m)%N) (mN : (m <= N)%N).
Hypotheses (ml : (m <= 4 ^ l)%N) (lm : (4 ^ l <= 4 * m)%N).
Hypotheses (psi0 : 0 < psi) (beta0 : 0 < beta) (beta1 : beta <= 1 / 2).
Hypothesis K1 : 1 <= K.
definition Lp source, line 1807
Type
forall {R : realType}, nat -> nat -> R
Definition
Definition Lp : R := 1 + ln (N%:R / m%:R).

Lp = ln (e N / m) and the exponent of the count of level k.

Used by 5 declarations in 1 file
definition Lz source, line 1808
Type
forall {R : realType}, nat -> nat -> R -> R
Definition
Definition Lz : R := 9 + ln (N%:R / m%:R) - ln beta.
Used by 3 declarations in 1 file
definition Hk source, line 1809
Type
forall {R : realType}, nat -> nat -> R -> nat -> R
Definition
Definition Hk k : R := 4 * m%:R / 4 ^+ k * (Lz + 3 * k%:R).
Used by 8 declarations in 1 file
definition uk source, line 1810
Type
forall {R : realType}, nat -> nat -> R -> R -> nat -> R
Definition
Definition uk k : R := ln 2 + 2 * Hk k + K * Num.sqrt m%:R * Lp.
Used by 6 declarations in 1 file
definition tk source, line 1812
Type
forall {R : realType}, nat -> nat -> R -> R -> R -> nat -> R
Definition
Definition tk k : R := 4 * psi * alpha m k * uk k + 8 * psi * Num.sqrt (uk k).

The thresholds of the union bound.

Used by 4 declarations in 1 file
lemma Lp_ge1 source, line 1814 
forall {R : realType} [N m : nat], (0 < m)%N -> (m <= N)%N -> 1 <= Lp N m
Statement as written in the source
Lemma Lp_ge1 : 1 <= Lp.
Used by 2 declarations in 1 file
lemma Lz_ge9 source, line 1822 
forall {R : realType} [N m : nat] [beta : R],
(0 < m)%N -> (m <= N)%N -> beta <= 1 / 2 -> 9 <= Lz N m beta
Statement as written in the source
Lemma Lz_ge9 : 9 <= Lz.
Used by 4 declarations in 1 file
lemma Hk_ge0 source, line 1832 
forall {R : realType} [N m : nat] [beta : R],
(0 < m)%N -> (m <= N)%N -> beta <= 1 / 2 -> forall k : nat, 0 <= Hk N m beta k
Statement as written in the source
Lemma Hk_ge0 k : 0 <= Hk k.
Used by 5 declarations in 1 file
lemma uk_gt0 source, line 1839 
forall {R : realType} [N m : nat] [beta K : R],
(0 < m)%N -> (m <= N)%N -> beta <= 1 / 2 -> 1 <= K -> forall k : nat, 0 < uk N m beta K k
Statement as written in the source
Lemma uk_gt0 k : 0 < uk k.
Used by 2 declarations in 1 file
lemma tk_gt0 source, line 1850 
forall {R : realType} [N m : nat] [psi beta K : R],
(0 < m)%N ->
(m <= N)%N -> 0 < psi -> beta <= 1 / 2 -> 1 <= K -> forall k : nat, 0 < tk N m psi beta K k
Statement as written in the source
Lemma tk_gt0 k : 0 < tk k.
Used by 1 declaration in 1 file
lemma tk_exp source, line 1859 
forall {R : realType} [N m : nat] [psi beta K : R],
(0 < m)%N ->
(m <= N)%N ->
0 < psi ->
beta <= 1 / 2 ->
1 <= K ->
forall k : nat,
expR
  (-
   minr (tk N m psi beta K k ^+ 2 / (64 * psi ^+ 2))
     (tk N m psi beta K k / (4 * (alpha m k * psi)))) <=
expR (- uk N m beta K k)
Statement as written in the source
Lemma tk_exp k : expR (- Num.min (tk k ^+ 2 / (64 * psi ^+ 2))
  (tk k / (4 * (alpha m k * psi)))) <= expR (- uk k).
Used by 1 declaration in 1 file
lemma Hk_step source, line 1887 
forall {R : realType} [N m : nat] [beta : R],
(0 < m)%N ->
(m <= N)%N -> beta <= 1 / 2 -> forall r : nat, Hk N m beta r.+1 <= Hk N m beta r / 2

Each level weighs at most half of the previous one.

Statement as written in the source
Lemma Hk_step r : Hk r.+1 <= Hk r / 2.
Used by 2 declarations in 1 file
lemma Hk_rev source, line 1901 
forall {R : realType} [N m l : nat] [beta : R],
(0 < m)%N ->
(m <= N)%N ->
beta <= 1 / 2 ->
forall [d : nat],
(d <= l)%N -> \sum_(j < d) Hk N m beta (l - j) <= 2 * Hk N m beta (l - d).+1
Statement as written in the source
Lemma Hk_rev d : (d <= l)%N -> \sum_(j < d) Hk (l - j) <= 2 * Hk (l - d).+1.
Used by 1 declaration in 1 file
lemma Hk_sum source, line 1909 
forall {R : realType} [N m l : nat] [beta : R],
(0 < m)%N ->
(m <= N)%N ->
beta <= 1 / 2 ->
forall [k : nat], (k <= l)%N -> \sum_(k <= r < l.+1) Hk N m beta r <= 2 * Hk N m beta k
Statement as written in the source
Lemma Hk_sum k : (k <= l)%N -> \sum_(k <= r < l.+1) Hk r <= 2 * Hk k.
lemma conf_size source, line 1932 
forall {R : realType} [N m l : nat] [beta : R],
(0 < m)%N ->
(m <= N)%N ->
0 < beta ->
beta <= 1 / 2 ->
forall [k : nat],
(k <= l)%N ->
(size (wconf N m beta k ++ xconf N m l beta k))%:R <= 2 * expR (2 * Hk N m beta k)
Statement as written in the source
Lemma conf_size k : (k <= l)%N ->
  (size (@wconf R N m beta k ++ @xconf R N m l beta k))%:R <=
  2 * expR (2 * Hk k).
Used by 1 declaration in 1 file
lemma tk_sum source, line 1960 
forall {R : realType} [N m l : nat] [psi beta K : R],
(0 < m)%N ->
(m <= N)%N ->
(4 ^ l <= 4 * m)%N ->
0 < psi ->
beta <= 1 / 2 ->
1 <= K ->
\sum_(0 <= k < l.+1) tk N m psi beta K k <=
2100 * K * psi * Num.ExtraDef.sqrtr m%:R * (Lp N m - ln beta)
Statement as written in the source
Lemma tk_sum : \sum_(0 <= k < l.+1) tk k <=
  2100 * K * psi * Num.sqrt m%:R * (Lp - ln beta).
Used by 1 declaration in 1 file
sectionrestricted_isometry
Context {R : realType} (N n m : nat) (mu : nat -> probability 'rV[R]_n R)
  (psi : R).
Hypothesis psi0 : 0 < psi.
Hypothesis sub : forall i (y : 'rV[R]_n), (i < N)%N -> mxdot y y = 1 ->
  subexponential (mu i) (fun v => mxdot v y) psi.
Hypothesis cen : forall i (y : 'rV[R]_n), (i < N)%N -> mxdot y y = 1 ->
  \int[mu i]_v mxdot v y = 0.
definition rip_T main result source, line 2140
Type
forall {R : realType}, nat -> nat -> R -> R -> R -> R
Definition
Definition rip_T (beta K : R) : R :=
  2100 * K * psi * Num.sqrt m%:R * (1 + ln (N%:R / m%:R) - ln beta).

The scale T = 2100 K psi sqrt m (ln (e N / m) + ln (1 / beta)).

Main result

Stated in the README together with restricted_isometry.

Used by 1 declaration in 1 file
theorem restricted_isometry main result source, line 2145 
forall {R : realType} [N n m : nat] [mu : nat -> probability 'rV_n R] [psi : R],
0 < psi ->
(forall (i : nat) (y : 'rV_n),
 (i < N)%N -> mxdot y y = 1 -> subexponential (mu i) ((mxdot (n:=n))^~ y) psi) ->
(forall (i : nat) (y : 'rV_n), (i < N)%N -> mxdot y y = 1 -> \int[mu i]_v mxdot v y = 0) ->
forall [beta K : R],
(0 < m)%N ->
(m <= N)%N ->
0 < beta ->
beta <= 1 / 2 ->
1 <= K ->
exists G : set (N.-tuple 'rV_n),
  [/\ (measure_tuple_display (measure_matrix_display default_measure_display)).-measurable
        G,
      (tuple_prod mu N (~` G) <=
       (2 * (trunc_log 4 m).+2%:R *
        expR (- (K * Num.ExtraDef.sqrtr m%:R * (1 + ln (N%:R / m%:R)))))%:E)%E
    & forall x : N.-tuple 'rV_n,
      G x ->
      rip_const m x <=
      256 * rip_T N m psi beta K ^+ 2 + 32 * rip_T N m psi beta K * maxnorm x +
      8 * beta * maxnorm x ^+ 2]

Theorem 5.1 of Adamczak, Litvak, Pajor and Tomczak-Jaegermann for psi_1 columns, with explicit constants.

Main result, as the README states it

Theorem 5.1 of Adamczak, Litvak, Pajor and Tomczak-Jaegermann at r = 1, with explicit constants. Let x_1, ..., x_N in 'rV[R]_n be independent (tuple_prod mu N), with every linear form <x_i, y>, |y| = 1, centered and subexponential with constant psi. For 1 <= m <= N, 0 < beta <= 1/2 and K >= 1, outside a measurable event of probability at most 2 (log_4 m + 2) exp (- K sqrt m (1 + ln (N / m))), every m-sparse u of norm at most one satisfies ||sum_i u_i x_i|^2 - sum_i u_i^2 |x_i|^2| <= 256 T^2 + 32 T C + 8 beta C^2, where T = 2100 K psi sqrt m (1 + ln (N / m) - ln beta) and C = max_i |x_i|.

Statement as written in the source
Theorem restricted_isometry (beta K : R) : (0 < m)%N -> (m <= N)%N ->
  0 < beta -> beta <= 1 / 2 -> 1 <= K ->
  exists G : set (N.-tuple 'rV[R]_n), [/\ measurable G,
    (tuple_prod mu N (~` G) <= (2 * (trunc_log 4 m).+2%:R *
      expR (- (K * Num.sqrt m%:R * (1 + ln (N%:R / m%:R)))))%:E)%E &
    forall x, G x -> rip_const m x <=
      256 * rip_T beta K ^+ 2 + 32 * rip_T beta K * maxnorm x +
      8 * beta * maxnorm x ^+ 2].
sectionsparse_consequences
Context {R : realType} (N n : nat) (x : N.-tuple 'rV[R]_n).
definition sqnorm_dev main result source, line 2217
Type
forall {R : realType} [N n : nat], N.-tuple 'rV_n -> R
Definition
Definition sqnorm_dev : R :=
  \big[Num.max/0]_i `|mxdot (tnth x i) (tnth x i) - 1|.

The largest deviation of the squared norms |x_i|^2 from 1.

Main result

Stated in the README together with sparse_isometry_dev.

Used by 3 declarations in 1 file
lemma sqnorm_dev_ge0 source, line 2220 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n), 0 <= sqnorm_dev x
Statement as written in the source
Lemma sqnorm_dev_ge0 : 0 <= sqnorm_dev.
lemma sqnorm_dev_ub source, line 2225 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) (i : 'I_N),
`|mxdot (tnth x i) (tnth x i) - 1| <= sqnorm_dev x
Statement as written in the source
Lemma sqnorm_dev_ub i : `|mxdot (tnth x i) (tnth x i) - 1| <= sqnorm_dev.
Used by 1 declaration in 1 file
lemma sparse_isometry_dev main result source, line 2230 
forall {R : realType} [N n : nat] (x : N.-tuple 'rV_n) [m : nat] [u : 'rV_N],
(#|supp u| <= m)%N ->
`|mxdot (u *m tuple_mx x) (u *m tuple_mx x) - mxdot u u| <=
(rip_const m x + sqnorm_dev x) * mxdot u u

The isometry defect on m-sparse vectors: the off-diagonal part is bounded by rip_const and the diagonal part by sqnorm_dev.

Main result, as the README states it

The restricted isometry constant: for every m-sparse u, ||sum_i u_i x_i|^2 - |u|^2| <= (rip_const m x + max_i ||x_i|^2 - 1|) |u|^2. Blocks: if |sum_i u_i x_i| <= L |u| for every m-sparse u, then |sum_i u_i x_i| <= L sqrt (N / m + 1) |u| for every u (deterministic).

Statement as written in the source
Lemma sparse_isometry_dev m (u : 'rV[R]_N) : (#|supp u| <= m)%N ->
  `|mxdot (u *m tuple_mx x) (u *m tuple_mx x) - mxdot u u| <=
  (rip_const m x + sqnorm_dev) * mxdot u u.
lemma tuple_mx_blocks main result source, line 2252 
forall {R : realType} [N n : nat] [x : N.-tuple 'rV_n] [m : nat] [L : R],
(0 < m)%N ->
0 <= L ->
(forall u : 'rV_N, (#|supp u| <= m)%N -> frobenius (u *m tuple_mx x) <= L * frobenius u) ->
forall u : 'rV_N,
frobenius (u *m tuple_mx x) <= L * Num.ExtraDef.sqrtr (N %/ m).+1%:R * frobenius u

A bound on the m-sparse vectors extends to all vectors, by cutting the coordinates into N %/ m + 1 blocks of at most m consecutive indices.

Main result

Stated in the README together with sparse_isometry_dev.

Statement as written in the source
Lemma tuple_mx_blocks m (L : R) : (0 < m)%N -> 0 <= L ->
  (forall u : 'rV[R]_N, (#|supp u| <= m)%N ->
    frobenius (u *m tuple_mx x) <= L * frobenius u) ->
  forall u : 'rV[R]_N, frobenius (u *m tuple_mx x) <=
    L * Num.sqrt (N %/ m).+1%:R * frobenius u.
sectionsphere_nets
Context {R : realType}.
definition sphere_net_spec source, line 2317
Type
forall {R : realType} [k : nat], seq 'cV_k -> Prop
Definition
Definition sphere_net_spec k (S : seq 'cV[R]_k) :=
  [/\ forall y, y \in S -> frobenius y = 1,
    is_net (@unit_sphere R k) S 4^-1 & (size S)%:R <= (18 * expR 1) ^+ k :> R].

A 1/4-net of the unit sphere of 'cV[R]_k, of size at most (18 e)^k.

Used by 3 declarations in 1 file
definition sphere_net source, line 2321
Type
forall {R : realType} (k : nat), seq 'cV_k
Definition
Definition sphere_net k : seq 'cV[R]_k := xget [::] (@sphere_net_spec k).
Used by 2 declarations in 1 file
lemma sphere_netP source, line 2323 
forall {R : realType} (k : nat), sphere_net_spec (sphere_net k)
Statement as written in the source
Lemma sphere_netP k : sphere_net_spec (sphere_net k).
Used by 1 declaration in 1 file
sectioncolumns_of_subsets
Context {R : realType} (N n : nat).
Implicit Types (F : {set 'I_N}) (x : N.-tuple 'rV[R]_n).
definition tuple_submx source, line 2345
Type
forall {R : realType} [N n : nat] (F : {set 'I_N}), N.-tuple 'rV_n -> 'M_(n, #|F|)
Definition
Definition tuple_submx (F : {set 'I_N}) (x : N.-tuple 'rV[R]_n) :
    'M[R]_(n, #|F|) :=
  \matrix_(j, k) (tnth x (enum_val k)) 0 j.

The n x |F| matrix whose columns are the x_i, i in F, in the order of enum_val.

Used by 4 declarations in 1 file
lemma tuple_submx_mul source, line 2349 
forall {R : realType} [N n : nat] [F : {set 'I_N}] (x : N.-tuple 'rV_n) (w : 'cV_#|F|),
tuple_submx F x *m w = (sparse_emb w *m tuple_mx x)^T
Statement as written in the source
Lemma tuple_submx_mul F x (w : 'cV[R]_#|F|) :
  tuple_submx F x *m w = (sparse_emb w *m tuple_mx x)^T.
Used by 2 declarations in 1 file
lemma tuple_submx_proj source, line 2361 
forall {R : realType} [N n : nat] [F : {set 'I_N}] (x : N.-tuple 'rV_n) [z : 'rV_N],
supp z \subset F -> tuple_submx F x *m sparse_proj F z = (z *m tuple_mx x)^T
Statement as written in the source
Lemma tuple_submx_proj F x (z : 'rV[R]_N) : supp z \subset F ->
  tuple_submx F x *m sparse_proj F z = (z *m tuple_mx x)^T.
Used by 1 declaration in 1 file
lemma tuple_submx_net source, line 2367 
forall {R : realType} [N n : nat] [F : {set 'I_N}] [x : N.-tuple 'rV_n] 
  [U : seq 'cV_n] [V : seq 'cV_#|F|] [t : R],
0 <= t ->
sphere_net_spec U ->
sphere_net_spec V ->
(forall (u : 'cV[R]_n)
   (w : 'cV[R]_#|F|),
 u \in U -> w \in V -> `|mxdot (sparse_emb w *m tuple_mx x) u^T| <= t) ->
opnorm (tuple_submx F x) <= 2 * t

Bilinear values on nets of the unit spheres bound the operator norm of tuple_submx F x.

Statement as written in the source
Lemma tuple_submx_net F x (U : seq 'cV[R]_n) (V : seq 'cV[R]_#|F|) (t : R) :
  0 <= t -> sphere_net_spec U -> sphere_net_spec V ->
  (forall u w, u \in U -> w \in V ->
     `|mxdot (sparse_emb w *m tuple_mx x) u^T| <= t) ->
  opnorm (tuple_submx F x) <= 2 * t.
Used by 1 declaration in 1 file
sectionsparse_norm
Context {R : realType} (N n : nat) (mu : nat -> probability 'rV[R]_n R) (K : R).
Hypothesis K0 : 0 < K.

The vectors have centered subgaussian linear forms.

Hypothesis sub : forall i (y : 'rV[R]_n), (i < N)%N -> mxdot y y = 1 ->
  subgaussian (mu i) (fun v => mxdot v y) K.
Hypothesis cen : forall i (y : 'rV[R]_n), (i < N)%N -> mxdot y y = 1 ->
  \int[mu i]_v mxdot v y = 0.
let coef section-local source, line 2397 
Let coef (a : 'rV[R]_N) (k : nat) : R :=
  if insub k is Some i then a 0 i else 0.
Used by 2 declarations in 1 file
let coefE section-local source, line 2400 
Let coefE (a : 'rV[R]_N) (i : 'I_N) : coef a i = a 0 i.
Used by 1 declaration in 1 file
lemma tuple_mx_dot_tail main result source, line 2404 
forall {R : realType} [N n : nat] [mu : nat -> probability 'rV_n R] [K : R],
0 < K ->
(forall (i : nat) (y : 'rV_n),
 (i < N)%N -> mxdot y y = 1 -> subgaussian (mu i) ((mxdot (n:=n))^~ y) K) ->
(forall (i : nat) (y : 'rV_n), (i < N)%N -> mxdot y y = 1 -> \int[mu i]_v mxdot v y = 0) ->
forall [a : 'rV_N] [y : 'rV_n] [t : R],
mxdot a a = 1 ->
mxdot y y = 1 ->
0 <= t ->
(tuple_prod mu N [set x | (t <= `|mxdot (a *m tuple_mx x) y|)%R] <=
 (2 * expR (- (t ^+ 2 / (16 * K ^+ 2))))%:E)%E

Hoeffding's inequality for <sum_i a_i x_i, y> with |a| = |y| = 1.

Main result

Stated in the README together with sparse_norm_subgaussian.

Statement as written in the source
Lemma tuple_mx_dot_tail (a : 'rV[R]_N) (y : 'rV[R]_n) (t : R) :
  mxdot a a = 1 -> mxdot y y = 1 -> 0 <= t ->
  (tuple_prod mu N [set x | (t <= `|mxdot (a *m tuple_mx x) y|)%R] <=
   (2 * expR (- (t ^+ 2 / (16 * K ^+ 2))))%:E)%E.
Used by 1 declaration in 1 file
definition sparse_norm_bound main result source, line 2432
Type
forall {R : realType}, nat -> nat -> R -> nat -> R -> R
Definition
Definition sparse_norm_bound (m : nat) (s : R) : R :=
  8 * K * Num.sqrt (m%:R * (1 + ln (N%:R / m%:R)) + 6 * (m + n)%:R + s).

The bound of sparse_norm_subgaussian.

Main result

Stated in the README together with sparse_norm_subgaussian.

Used by 1 declaration in 1 file
theorem sparse_norm_subgaussian main result source, line 2438 
forall {R : realType} [N n : nat] [mu : nat -> probability 'rV_n R] [K : R],
0 < K ->
(forall (i : nat) (y : 'rV_n),
 (i < N)%N -> mxdot y y = 1 -> subgaussian (mu i) ((mxdot (n:=n))^~ y) K) ->
(forall (i : nat) (y : 'rV_n), (i < N)%N -> mxdot y y = 1 -> \int[mu i]_v mxdot v y = 0) ->
forall [m : nat] [s : R],
(0 < m)%N ->
(m <= N)%N ->
0 <= s ->
exists G : set (N.-tuple 'rV_n),
  [/\ (measure_tuple_display (measure_matrix_display default_measure_display)).-measurable
        G,
      (tuple_prod mu N (~` G) <= (2 * expR (- s))%:E)%E
    & forall x : N.-tuple 'rV_n,
      G x ->
      forall u : 'rV_N,
      (#|supp u| <= m)%N ->
      frobenius (u *m tuple_mx x) <= sparse_norm_bound N n K m s * frobenius u]

For independent x_1, ..., x_N with centered K-subgaussian linear forms, with probability at least 1 - 2 exp (- s), every m-sparse u satisfies |sum_i u_i x_i| <= 8 K sqrt (m (1 + ln (N / m)) + 6 (m + n) + s) |u|.

Main result, as the README states it

Norms of sparse combinations of independent subgaussian vectors: if x_1, ..., x_N in 'rV[R]_n are independent (tuple_prod mu N) with every linear form <x_i, y>, |y| = 1, centered and subgaussian with constant K, then for 1 <= m <= N and s >= 0, outside a measurable event of probability at most 2 exp (- s), every m-sparse u satisfies |sum_i u_i x_i| <= 8 K sqrt (m (1 + ln (N / m)) + 6 (m + n) + s) |u| (Vershynin's Theorem 4.4.5 with a union bound over the supports). For unit a and y, P(|<sum_i a_i x_i, y>| >= t) <= 2 exp (- t^2 / (16 K^2)).

Statement as written in the source
Theorem sparse_norm_subgaussian (m : nat) (s : R) :
  (0 < m)%N -> (m <= N)%N -> 0 <= s ->
  exists G : set (N.-tuple 'rV[R]_n), [/\ measurable G,
    (tuple_prod mu N (~` G) <= (2 * expR (- s))%:E)%E &
    forall x, G x -> forall u : 'rV[R]_N, (#|supp u| <= m)%N ->
      frobenius (u *m tuple_mx x) <= sparse_norm_bound m s * frobenius u].
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.