GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysismatrixcovering

Covering the nuclear-norm ball by products of column balls

GaussianAnalysis.matrix.coveringlibrary/matrix/covering.v508 lines14 lemmas and theorems, 2 definitionssource
Imports 15 library modules and 29 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.algebra.archimedean, 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 1 files of the paper proofs

Lemma 3.10 of Koehler and Sohn (arXiv 2608.27372, lines 2880-2948): for c0 d <= m, q <= C0 d, the m x q matrices of nuclear norm at most gam d are covered by C^(m q) translates of the product of q Euclidean balls of radius gam, one for each column, with C depending on c0 and C0 only. The paper bounds the volume of the nuclear-norm ball by Urysohn's inequality. Here the covering number is bounded in two steps (dual_ball_covering), for G = vec_mx g with g of law gauss (m * q):

  • Sudakov's minoration (sudakov.v) covers the set K by Frobenius balls of radius lam = sqrt (r gam), since E max over K of <G, A> is at most r E opnorm G <= r (sqrt m + sqrt q) (escape.v);
  • the dual Sudakov inequality covers each such ball by products of column balls of radius gam, since E colmax G <= E opnorm G.

The nuclear norm enters only through the duality <A, B> <= r opnorm B, so the results hold for every set K with this property.

  • dual_ball_covering: for m, q > 0, r, gam > 0 and K with <A, B> <= r opnorm B for every A in K and every B, there are at most exp (48 (m + q) r / gam + 33) matrices such that every A in K is within gam of one of them for colmax.
  • product_covering (Lemma 3.10): with r = gam d, d > 0, c0 > 0 and c0 d <= m, q <= C0 d, at most exp ((96 C0 + 33) / c0^2) ^ (m q) of them.
  • matrix_small_ball, the covering step of Lemma 3.14 (lines 3498-3548): for distinct coordinates y_(g i j), i < n, j < q, of a tuple y of independent coordinates, and w_i in 'rV_m, if every column sum sum_i y_(g i j) w_i is within gam of any given vector with probability at most p, then colsum_mx g w y + B is in a measurable K as above with probability at most exp (48 (m + q) r / gam + 33) p^q: cover K, then use the independence of the columns.
colmax Amax_j |A e_j|, the largest Euclidean norm of a column of A, the norm of A from l^1 to l^2
colsum_mx g w ythe m x q matrix whose column j is sum_i y_(g i j) w_i

Main results

ResultsStatement
product_coveringdual_ball_coveringcolmax
Lemma 3.10 of Koehler and Sohn: if c0 d <= m, q <= C0 d with c0 > 0 and d > 0, the m x q matrices of nuclear norm at most gam d (written by duality: <A, B> <= gam d opnorm B for every B) are covered by exp ((96 C0 + 33) / c0^2) ^ (m q) translates of the product of the column balls of radius gam (the ball of colmax, the largest Euclidean norm of a column). In general, a set K with <A, B> <= r opnorm B on K has such a covering of size exp (48 (m + q) r / gam + 33). Proved by Sudakov's minoration and the dual Sudakov inequality instead of Urysohn's inequality.
matrix_small_ballcolsum_mx
Small-ball probability of a random matrix with independent columns (the covering step of Lemma 3.14 of Koehler and Sohn): for distinct coordinates y_(g i j), i < n, j < q, of a tuple y of law tuple_prod mu N, and w_i in 'rV_m, if each column sum sum_i y_(g i j) w_i is within gam of any given vector with probability at most p, then the m x q matrix of these columns plus a fixed B lies in a measurable K with <A, C> <= r opnorm C on K (the nuclear-norm ball of radius r, for instance) with probability at most exp (48 (m + q) r / gam + 33) p^q.

Declarations16 exported, 6 local

lemma, theoremdefinitioninstancelocal
sectioncolmax
Context {R : realType} {m q : nat}.
Implicit Types A B : 'M[R]_(m, q).
definition colmax main result source, line 73
Type
forall {R : realType} {m q : nat}, 'M_(m, q) -> R
Definition
Definition colmax A : R := \big[maxr/0]_(j < q) frobenius (col j A).

The largest Euclidean norm of a column, the norm of A as an operator from l^1 to l^2.

Main result

Stated in the README together with product_covering.

Used by 15 declarations in 1 file
lemma colmax_ge0 source, line 75 
forall {R : realType} {m q : nat} (A : 'M_(m, q)), 0 <= colmax A
Statement as written in the source
Lemma colmax_ge0 A : 0 <= colmax A.
Used by 1 declaration in 1 file
lemma colmax_col source, line 82 
forall {R : realType} {m q : nat} (A : 'M_(m, q)) (j : 'I_q),
frobenius (col j A) <= colmax A
Statement as written in the source
Lemma colmax_col A j : frobenius (col j A) <= colmax A.
Used by 2 declarations in 1 file
lemma colmax_le source, line 85 
forall {R : realType} {m q : nat} [A : 'M_(m, q)]
  [c : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R],
0 <= c -> (forall j : 'I_q, frobenius (col j A) <= c) -> colmax A <= c
Statement as written in the source
Lemma colmax_le A c : 0 <= c -> (forall j, frobenius (col j A) <= c) ->
  colmax A <= c.
Used by 2 declarations in 1 file
lemma colmaxN source, line 89 
forall {R : realType} {m q : nat} (A : 'M_(m, q)), colmax (- A) = colmax A
Statement as written in the source
Lemma colmaxN A : colmax (- A) = colmax A.
Used by 3 declarations in 1 file
lemma colmaxD source, line 92 
forall {R : realType} {m q : nat} (A B : 'M_(m, q)), colmax (A + B) <= colmax A + colmax B
Statement as written in the source
Lemma colmaxD A B : colmax (A + B) <= colmax A + colmax B.
Used by 2 declarations in 1 file
lemma colmaxZ source, line 99 
forall {R : realType} {m q : nat} [c : R] (A : 'M_(m, q)),
0 <= c -> colmax (c *: A) = c * colmax A
Statement as written in the source
Lemma colmaxZ (c : R) A : 0 <= c -> colmax (c *: A) = c * colmax A.
Used by 2 declarations in 1 file
lemma colmax_le_opnorm source, line 106 
forall {R : realType} {m q : nat} (A : 'M_(m, q)), colmax A <= opnorm A
Statement as written in the source
Lemma colmax_le_opnorm A : colmax A <= opnorm A.
Used by 2 declarations in 1 file
lemma colmax_le_frobenius source, line 113 
forall {R : realType} {m q : nat} (A : 'M_(m, q)), colmax A <= frobenius A
Statement as written in the source
Lemma colmax_le_frobenius A : colmax A <= frobenius A.
Used by 2 declarations in 1 file
lemma colmax_lipschitz source, line 116 
forall {R : realType} {m q : nat} (A B : 'M_(m, q)),
`|colmax A - colmax B| <= colmax (A - B)
Statement as written in the source
Lemma colmax_lipschitz A B : `|colmax A - colmax B| <= colmax (A - B).
Used by 2 declarations in 1 file
sectiondual_ball_covering
Context {R : realType} {m q : nat}.
let mxdot_vec_mx section-local source, line 131 
Let mxdot_vec_mx (g : 'rV[R]_(m * q)) (A : 'M[R]_(m, q)) :
  mxdot (vec_mx g) A = mxdot g (mxvec A).
Used by 1 declaration in 1 file
let frobenius_mxvec_mx section-local source, line 138 
Let frobenius_mxvec_mx (A : 'M[R]_(m, q)) :
  frobenius (mxvec A) = frobenius A.
Used by 2 declarations in 1 file
let gopnorm_mean section-local source, line 143 
Let gopnorm_mean : (0 < m)%N -> (0 < q)%N ->
  \int[gauss (m * q)]_g colmax (vec_mx g : 'M[R]_(m, q)) <=
  Num.sqrt m%:R + Num.sqrt q%:R.

E opnorm G <= sqrt m + sqrt q, for G = vec_mx g of law gauss (m * q).

Used by 1 declaration in 1 file
let colmax0 section-local source, line 161 
Let colmax0 : colmax (0 : 'M[R]_(m, q)) = 0.
Used by 1 declaration in 1 file
let frob_sep section-local source, line 166 
Let frob_sep (K : set 'M[R]_(m, q)) (r lam : R) (s : seq 'M[R]_(m, q)) :
  (0 < m)%N -> (0 < q)%N -> 0 <= r -> 0 < lam ->
  (forall A, K A -> forall B, mxdot A B <= r * opnorm B) ->
  separated (fun A B => frobenius (A - B)) K lam s ->
  (size s)%:R <=
  expR ((2 * Num.sqrt 2 * r * (Num.sqrt m%:R + Num.sqrt q%:R) / lam + 4) ^+ 2).
Used by 1 declaration in 1 file
let colmax_sep section-local source, line 217 
Let colmax_sep (lam gam : R) (s : seq 'M[R]_(m, q)) :
  (0 < m)%N -> (0 < q)%N -> 0 < gam ->
  separated (fun A B => colmax (A - B)) [set B | frobenius B <= lam] gam s ->
  (size s)%:R <=
  2 * expR (8 * lam ^+ 2 * (Num.sqrt m%:R + Num.sqrt q%:R) ^+ 2 / gam ^+ 2).
Used by 1 declaration in 1 file
theorem dual_ball_covering main result source, line 254 
forall {R : realType} {m q : nat} [K : set 'M_(m, q)] [r gam : R],
(0 < m)%N ->
(0 < q)%N ->
0 < r ->
0 < gam ->
(forall A : 'M_(m, q), K A -> forall B : 'M_(m, q), mxdot A B <= r * opnorm B) ->
exists N : seq 'M_(m, q),
  (size N)%:R <= expR (48 * (m + q)%:R * r / gam + 33) /\
  (forall A : 'M_(m, q),
   K A ->
   exists2 B : 'M[R]_(m, q),
     B \in N & colmax (A - B) <= gam)

Covering a set K of matrices on which every linear form is bounded by r times the operator norm (a set contained in the ball of radius r of the nuclear norm) by products of Euclidean balls of radius gam, one for each column: at most exp (48 (m + q) r / gam + 33) of them suffice.

Main result

Stated in the README together with product_covering.

Statement as written in the source
Theorem dual_ball_covering (K : set 'M[R]_(m, q)) (r gam : R) :
  (0 < m)%N -> (0 < q)%N -> 0 < r -> 0 < gam ->
  (forall A, K A -> forall B, mxdot A B <= r * opnorm B) ->
  exists N : seq 'M[R]_(m, q),
    (size N)%:R <= expR (48 * (m + q)%:R * r / gam + 33) /\
    forall A, K A -> exists2 B, B \in N & colmax (A - B) <= gam.
Used by 2 declarations in 1 file
corollary product_covering main result source, line 337 
forall {R : realType} {m q : nat} [c0 C0 gam : R] [d : nat] [K : set 'M_(m, q)],
0 < c0 ->
(0 < d)%N ->
0 < gam ->
c0 * d%:R <= m%:R ->
c0 * d%:R <= q%:R ->
m%:R <= C0 * d%:R ->
q%:R <= C0 * d%:R ->
(forall A : 'M_(m, q), K A -> forall B : 'M_(m, q), mxdot A B <= gam * d%:R * opnorm B) ->
exists N : seq 'M_(m, q),
  (size N)%:R <= expR ((96 * C0 + 33) / c0 ^+ 2) ^+ (m * q) /\
  (forall A : 'M_(m, q),
   K A ->
   exists2 B : 'M[R]_(m, q),
     B \in N & colmax (A - B) <= gam)

Lemma 3.10 of Koehler and Sohn: when c0 d <= m, q <= C0 d, the matrices of nuclear norm at most gam d (written by duality with opnorm) are covered by C^(m q) products of column balls of radius gam, with C = exp ((96 C0 + 33) / c0^2).

Main result, as the README states it

Lemma 3.10 of Koehler and Sohn: if c0 d <= m, q <= C0 d with c0 > 0 and d > 0, the m x q matrices of nuclear norm at most gam d (written by duality: <A, B> <= gam d opnorm B for every B) are covered by exp ((96 C0 + 33) / c0^2) ^ (m q) translates of the product of the column balls of radius gam (the ball of colmax, the largest Euclidean norm of a column). In general, a set K with <A, B> <= r opnorm B on K has such a covering of size exp (48 (m + q) r / gam + 33). Proved by Sudakov's minoration and the dual Sudakov inequality instead of Urysohn's inequality.

Statement as written in the source
Corollary product_covering (c0 C0 gam : R) (d : nat) (K : set 'M[R]_(m, q)) :
  0 < c0 -> (0 < d)%N -> 0 < gam ->
  c0 * d%:R <= m%:R -> c0 * d%:R <= q%:R ->
  m%:R <= C0 * d%:R -> q%:R <= C0 * d%:R ->
  (forall A, K A -> forall B, mxdot A B <= gam * d%:R * opnorm B) ->
  exists N : seq 'M[R]_(m, q),
    (size N)%:R <= expR ((96 * C0 + 33) / c0 ^+ 2) ^+ (m * q) /\
    forall A, K A -> exists2 B, B \in N & colmax (A - B) <= gam.
sectionmatrix_small_ball
Context {R : realType} {m q : nat}.
definition colsum_mx main result source, line 384
Type
forall {R : realType} {m q : nat} [N n : nat],
('I_n -> 'I_q -> 'I_N) -> (nat -> 'rV_m) -> N.-tuple (measurableTypeR R) -> 'M_(m, q)
Definition
Definition colsum_mx N n (g : 'I_n -> 'I_q -> 'I_N) (w : nat -> 'rV[R]_m)
    (y : N.-tuple (measurableTypeR R)) : 'M[R]_(m, q) :=
  \matrix_(a, j) \sum_(i < n) tnth y (g i j) * w i 0 a.

The m x q matrix whose column j is sum_i y_(g i j) w_i, for an N-tuple y and a layout g of n rows and q columns of its coordinates.

Main result

Stated in the README together with matrix_small_ball.

Used by 3 declarations in 1 file
lemma colsum_mx_col source, line 388 
forall {R : realType} {m q : nat} [N n : nat] (g : 'I_n -> 'I_q -> 'I_N) 
  (w : nat -> 'rV_m) (y : N.-tuple (measurableTypeR R)) (j : 'I_q),
(col j (colsum_mx g w y))^T = \sum_(i < n) tnth (tuple_pick (g^~ j) y) i *: w i
Statement as written in the source
Lemma colsum_mx_col N n (g : 'I_n -> 'I_q -> 'I_N) w
    (y : N.-tuple (measurableTypeR R)) (j : 'I_q) :
  (col j (colsum_mx g w y))^T =
  \sum_(i < n) tnth (tuple_pick (g^~ j) y) i *: w i.
Used by 1 declaration in 1 file
lemma measurable_colsum_mx source, line 397 
forall {R : realType} {m q : nat} [N n : nat] (g : 'I_n -> 'I_q -> 'I_N) (w : nat -> 'rV_m),
measurable_fun [set: N.-tuple _]
  (colsum_mx g w)
Statement as written in the source
Lemma measurable_colsum_mx N n (g : 'I_n -> 'I_q -> 'I_N) w :
  measurable_fun setT (colsum_mx g w).
Used by 1 declaration in 1 file
Local Open Scope ereal_scope.
theorem matrix_small_ball main result source, line 419 
forall {R : realType} {m q : nat} [N n : nat] [g : 'I_n -> 'I_q -> 'I_N]
  [mu : nat -> probability (measurableTypeR R) R] [w : nat -> 'rV_m] 
  (B : 'M_(m, q)) [K : set 'M_(m, q)] [r gam p : R],
(forall (i : 'I_n) (j : 'I_q) (i' : 'I_n) (j' : 'I_q), g i j = g i' j' -> i = i' /\ j = j') ->
(0 < m)%N ->
(0 < q)%N ->
0 < r ->
0 < gam ->
0 <= p ->
(measure_matrix_display default_measure_display).-measurable K ->
(forall A : 'M_(m, q), K A -> forall C : 'M_(m, q), mxdot A C <= r * opnorm C) ->
(forall (j : 'I_q) (nu : nat -> probability (measurableTypeR R) R),
 (forall i : 'I_n, nu i = mu (g i j)) ->
 forall z : 'rV_m,
 (tuple_prod nu n [set s | (frobenius (\sum_(i < n) tnth s i *: w i - z) <= gam)%R] <= p%:E)%E) ->
(tuple_prod mu N [set y | K (colsum_mx g w y + B)%R] <=
 (expR (48 * (m + q)%:R * r / gam + 33) * p ^+ q)%:E)%E

Small-ball probability of a random matrix with independent columns. The entries y_(g i j) are distinct coordinates of a tuple y of law tuple_prod mu N. If, for every column j, the sum sum_i y_(g i j) w_i is within gam of any given vector with probability at most p, then the matrix colsum_mx g w y + B lies in a measurable set K with <A, C> <= r opnorm C on K with probability at most exp (48 (m + q) r / gam + 33) p^q: cover K by that many products of column balls (dual_ball_covering) and use the independence of the columns.

Main result, as the README states it

Small-ball probability of a random matrix with independent columns (the covering step of Lemma 3.14 of Koehler and Sohn): for distinct coordinates y_(g i j), i < n, j < q, of a tuple y of law tuple_prod mu N, and w_i in 'rV_m, if each column sum sum_i y_(g i j) w_i is within gam of any given vector with probability at most p, then the m x q matrix of these columns plus a fixed B lies in a measurable K with <A, C> <= r opnorm C on K (the nuclear-norm ball of radius r, for instance) with probability at most exp (48 (m + q) r / gam + 33) p^q.

Statement as written in the source
Theorem matrix_small_ball N n (g : 'I_n -> 'I_q -> 'I_N)
    (mu : nat -> probability (measurableTypeR R) R)
    (w : nat -> 'rV[R]_m) (B : 'M[R]_(m, q)) (K : set 'M[R]_(m, q))
    (r gam p : R) :
  (forall i j i' j', g i j = g i' j' -> i = i' /\ j = j') ->
  (0 < m)%N -> (0 < q)%N -> (0 < r)%R -> (0 < gam)%R -> (0 <= p)%R ->
  measurable K ->
  (forall A, K A -> forall C, mxdot A C <= r * opnorm C)%R ->
  (forall (j : 'I_q) (nu : nat -> probability (measurableTypeR R) R),
     (forall i : 'I_n, nu i = mu (g i j)) -> forall z : 'rV[R]_m,
     tuple_prod nu n
       [set s | (frobenius (\sum_(i < n) tnth s i *: w i - z) <= gam)%R]
     <= p%:E) ->
  tuple_prod mu N [set y | K (colsum_mx g w y + B)%R] <=
    (expR (48 * (m + q)%:R * r / gam + 33) * p ^+ q)%: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.