GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysismatrixnets

Nets in Euclidean spaces

GaussianAnalysis.matrix.netslibrary/matrix/nets.v471 lines28 lemmas and theorems, 8 definitionssource
Imports 3 library modules and 14 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, mathcomp.algebra.archimedean, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.reals.reals, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 8
Required by 6 files of the paper proofs

A finite eps-net of a set S of column vectors is a finite sequence N such that every point of S lies within Euclidean distance eps of a point of N. The operator norm of a matrix is controlled by its values on a net of the unit ball or of the unit sphere (opnorm_net, opnorm_net_bilinear, opnorm_net_sphere, opnorm_net_sym). Every set in the ball of radius r of 'cV[R]_n has an eps-net of at most (2 e (1 + 2 r / eps))^n of its own points (net_exists, unit_ball_net, unit_sphere_net). The proof rounds each point to a grid of mesh h = eps / (2 sqrt n) and counts the grid points: a point of the ball has at most 2^n C(n + k, n) possible roundings, with k = floor(2 n r / eps).

is_net S N epsevery x in S has a point y of N with frobenius (x - y) <= eps
unit_ball nthe closed unit ball [set x | frobenius x <= 1] of 'cV[R]_n
unit_sphere nthe unit sphere [set x | frobenius x = 1] of 'cV[R]_n
budget n kthe lists of n natural numbers with sum at most k
sign_lists nthe lists of n booleans
grid_point h (a, s)the column with coordinates (-1)^(s_i) h a_i
grid_code h xthe code (a, s) of the column x: a_i is the integer part of |x_i| / h, and s_i says whether x_i < 0
grid_codes n kthe codes (a, s) with a in budget n k

Main results

ResultsStatementUsed by theories/
opnorm_netopnorm_net_bilinearopnorm_net_sphereopnorm_net_sym
If N is an eps-net of the unit ball, then opnorm A <= max_{y in N} |A y| / (1 - eps), opnorm A <= max_{u, v in N} |u^T A v| / (1 - 2 eps), and for symmetric A, opnorm A <= max_{v in N} |v^T A v| / (1 - 2 eps). The bilinear bound also holds for nets of the unit sphere.Spectral/OperatorNet (opnorm_net_sphere); comparison/escape.v in the library. The other three are used inside the library only
net_existsunit_ball_netunit_sphere_net
Every set in the ball of radius r of 'cV[R]_n has an eps-net of at most (2 e (1 + 2 r / eps))^n of its own points; for the unit ball and the unit sphere, r = 1. Proved by rounding to a grid of mesh eps / (2 sqrt n) and counting the grid points.Spectral/OperatorNet (unit_sphere_net); comparison/escape.v in the library
bin_le_expRsize_budget
C(m, n) <= (e m / n)^n. There are C(n + k, n) lists of n natural numbers with sum at most k.through net_exists

Declarations36 exported

lemma, theoremdefinitioninstancelocal
sectionnets
Variable R : realType.
Implicit Types m n : nat.
definition is_net source, line 49
Type
forall [R : realType] [n : nat], set 'cV_n -> seq 'cV_n -> R -> Prop
Definition
Definition is_net n (S : set 'cV[R]_n) (N : seq 'cV[R]_n) (eps : R) :=
  forall x, S x -> exists2 y, y \in N & frobenius (x - y) <= eps.
Used by 14 declarations in 4 files
definition unit_ball source, line 52
Type
forall [R : realType] [n : nat], set 'cV_n
Definition
Definition unit_ball n : set 'cV[R]_n := [set x | frobenius x <= 1].
Used by 27 declarations in 3 files
lemma unit_ball0 source, line 54 
forall (R : realType) (n : nat), unit_ball 0
Statement as written in the source
Lemma unit_ball0 n : @unit_ball n 0.
Used by 4 declarations in 2 files
definition unit_sphere source, line 57
Type
forall [R : realType] [n : nat], set 'cV_n
Definition
Definition unit_sphere n : set 'cV[R]_n := [set x | frobenius x = 1].
Used by 11 declarations in 3 files
lemma unit_sphere_ball source, line 59 
forall [R : realType] [n : nat], unit_sphere (n:=n) `<=` unit_ball (n:=n)
Statement as written in the source
Lemma unit_sphere_ball n : @unit_sphere n `<=` @unit_ball n.
Used by 2 declarations in 1 file
lemma is_net_sub source, line 62 
forall [R : realType] [n : nat] [S0 T : set 'cV_n] [N : seq 'cV_n] [eps : R],
S0 `<=` T -> is_net T N eps -> is_net S0 N eps
Statement as written in the source
Lemma is_net_sub n (S T : set 'cV[R]_n) N eps :
  S `<=` T -> is_net T N eps -> is_net S N eps.
Used by 1 declaration in 1 file
lemma is_net_le source, line 66 
forall [R : realType] [n : nat] [S0 : set 'cV_n] [N : seq 'cV_n] [eps eps' : R],
eps <= eps' -> is_net S0 N eps -> is_net S0 N eps'
Statement as written in the source
Lemma is_net_le n (S : set 'cV[R]_n) N eps eps' :
  eps <= eps' -> is_net S N eps -> is_net S N eps'.
lemma opnorm_net main result source, line 71 
forall [R : realType] [m n : nat] [A : 'M_(m, n)] [N : seq 'cV_n] [eps b : R],
0 <= eps < 1 ->
is_net (unit_ball (n:=n)) N eps ->
(forall y : 'cV[R]_n,
 y \in N -> frobenius (A *m y) <= b) ->
opnorm A <= b / (1 - eps)

The values of A on a net of the unit ball control its operator norm.

Main result, as the README states it

If N is an eps-net of the unit ball, then opnorm A <= max_{y in N} |A y| / (1 - eps), opnorm A <= max_{u, v in N} |u^T A v| / (1 - 2 eps), and for symmetric A, opnorm A <= max_{v in N} |v^T A v| / (1 - 2 eps). The bilinear bound also holds for nets of the unit sphere.

Used in theories/ by: Spectral/OperatorNet (opnorm_net_sphere); comparison/escape.v in the library. The other three are used inside the library only
Statement as written in the source
Lemma opnorm_net m n (A : 'M[R]_(m, n)) (N : seq 'cV[R]_n) (eps b : R) :
  0 <= eps < 1 -> is_net (@unit_ball n) N eps ->
  (forall y, y \in N -> frobenius (A *m y) <= b) ->
  opnorm A <= b / (1 - eps).
lemma mxdot_net_bound source, line 85 
forall [R : realType] [m n : nat] (A : 'M_(m, n)) [y u : 'cV_m] [x : 'cV_n] (v : 'cV_n),
frobenius y <= 1 ->
frobenius x <= 1 ->
frobenius u <= 1 ->
`|mxdot y (A *m x)| <=
`|mxdot u (A *m v)| + opnorm A * (frobenius (y - u) + frobenius (x - v))
Statement as written in the source
Lemma mxdot_net_bound m n (A : 'M[R]_(m, n)) (y u : 'cV[R]_m) (x v : 'cV[R]_n) :
  frobenius y <= 1 -> frobenius x <= 1 -> frobenius u <= 1 ->
  `|mxdot y (A *m x)| <=
    `|mxdot u (A *m v)| + opnorm A * (frobenius (y - u) + frobenius (x - v)).
Used by 2 declarations in 1 file
lemma opnorm_net_sphere main result source, line 103 
forall [R : realType] [m n : nat] [A : 'M_(m, n)] [U : seq 'cV_m] 
  [V : seq 'cV_n] [eps b : R],
0 <= eps ->
2 * eps < 1 ->
0 <= b ->
is_net (unit_sphere (n:=m)) U eps ->
(forall u : 'cV[R]_m, u \in U -> frobenius u <= 1) ->
is_net (unit_sphere (n:=n)) V eps ->
(forall (u : 'cV[R]_m)
   (v : 'cV[R]_n),
 u \in U -> v \in V -> `|mxdot u (A *m v)| <= b) ->
opnorm A <= b / (1 - 2 * eps)

Bilinear values on nets of both unit spheres control the operator norm.

Main result

Stated in the README together with opnorm_net.

Statement as written in the source
Lemma opnorm_net_sphere m n (A : 'M[R]_(m, n)) (U : seq 'cV[R]_m)
    (V : seq 'cV[R]_n) (eps b : R) :
  0 <= eps -> 2 * eps < 1 -> 0 <= b ->
  is_net (@unit_sphere m) U eps -> (forall u, u \in U -> frobenius u <= 1) ->
  is_net (@unit_sphere n) V eps ->
  (forall u v, u \in U -> v \in V -> `|mxdot u (A *m v)| <= b) ->
  opnorm A <= b / (1 - 2 * eps).
Used by 3 declarations in 3 files
lemma opnorm_net_bilinear main result source, line 145 
forall [R : realType] [m n : nat] [A : 'M_(m, n)] [U : seq 'cV_m] 
  [V : seq 'cV_n] [eps b : R],
0 <= eps ->
2 * eps < 1 ->
is_net (unit_ball (n:=m)) U eps ->
(forall u : 'cV[R]_m, u \in U -> frobenius u <= 1) ->
is_net (unit_ball (n:=n)) V eps ->
(forall (u : 'cV[R]_m)
   (v : 'cV[R]_n),
 u \in U -> v \in V -> `|mxdot u (A *m v)| <= b) ->
opnorm A <= b / (1 - 2 * eps)

Bilinear values on nets of both unit balls control the operator norm.

Main result

Stated in the README together with opnorm_net.

Statement as written in the source
Lemma opnorm_net_bilinear m n (A : 'M[R]_(m, n)) (U : seq 'cV[R]_m)
    (V : seq 'cV[R]_n) (eps b : R) :
  0 <= eps -> 2 * eps < 1 ->
  is_net (@unit_ball m) U eps -> (forall u, u \in U -> frobenius u <= 1) ->
  is_net (@unit_ball n) V eps ->
  (forall u v, u \in U -> v \in V -> `|mxdot u (A *m v)| <= b) ->
  opnorm A <= b / (1 - 2 * eps).
Used by 1 declaration in 1 file
lemma form_unit_ball_le source, line 160 
forall [R : realType] [n : nat] [A : 'M_n] [c : R],
(forall x : 'cV_n, frobenius x <= 1 -> `|mxdot x (A *m x)| <= c) ->
forall x : 'cV_n, `|mxdot x (A *m x)| <= c * mxdot x x
Statement as written in the source
Lemma form_unit_ball_le n (A : 'M[R]_n) (c : R) :
  (forall x : 'cV[R]_n, frobenius x <= 1 -> `|mxdot x (A *m x)| <= c) ->
  forall x : 'cV[R]_n, `|mxdot x (A *m x)| <= c * mxdot x x.
Used by 1 declaration in 1 file
lemma opnorm_net_sym main result source, line 177 
forall [R : realType] [n : nat] [A : 'M_n] [V : seq 'cV_n] [eps b : R],
A \is symmetricmx ->
0 <= eps ->
2 * eps < 1 ->
is_net (unit_ball (n:=n)) V eps ->
(forall v : 'cV[R]_n, v \in V -> frobenius v <= 1) ->
(forall v : 'cV[R]_n,
 v \in V -> `|mxdot v (A *m v)| <= b) ->
opnorm A <= b / (1 - 2 * eps)

Values of the quadratic form on a net of the unit ball control the operator norm of a symmetric matrix.

Main result

Stated in the README together with opnorm_net.

Statement as written in the source
Lemma opnorm_net_sym n (A : 'M[R]_n) (V : seq 'cV[R]_n) (eps b : R) :
  A \is symmetricmx -> 0 <= eps -> 2 * eps < 1 ->
  is_net (@unit_ball n) V eps -> (forall v, v \in V -> frobenius v <= 1) ->
  (forall v, v \in V -> `|mxdot v (A *m v)| <= b) ->
  opnorm A <= b / (1 - 2 * eps).
Used by 1 declaration in 1 file

Lists of natural numbers with a bounded sum, and lists of signs: the codes of the points of a grid.

sectioncodes
fixpoint budget source, line 202
Type
nat -> nat -> seq (seq nat)
Definition
Fixpoint budget (n k : nat) : seq (seq nat) :=
  if n is n'.+1 then
    flatten [seq [seq a :: t | t <- budget n' (k - a)] | a <- iota 0 k.+1]
  else [:: [::]].
Used by 3 declarations in 1 file
lemma mem_budget source, line 207 
forall [n k : nat] [a : seq nat], size a = n -> (sumn a <= k)%N -> a \in budget n k
Statement as written in the source
Lemma mem_budget n k (a : seq nat) :
  size a = n -> (sumn a <= k)%N -> a \in budget n k.
Used by 1 declaration in 1 file
lemma sum_bin_hockey source, line 219 
forall n k : nat, (\sum_(a < k.+1) 'C(n + (k - a), n))%N = 'C(n.+1 + k, n.+1)

The hockey-stick identity.

Statement as written in the source
Lemma sum_bin_hockey n k :
  (\sum_(a < k.+1) 'C(n + (k - a), n) = 'C(n.+1 + k, n.+1))%N.
Used by 1 declaration in 1 file
lemma size_budget main result source, line 228 
forall n k : nat, size (budget n k) = 'C(n + k, n)
Main result

Stated in the README together with bin_le_expR.

Statement as written in the source
Lemma size_budget n k : size (budget n k) = 'C(n + k, n).
Used by 1 declaration in 1 file
fixpoint sign_lists source, line 237
Type
nat -> seq (seq bool)
Definition
Fixpoint sign_lists (n : nat) : seq (seq bool) :=
  if n is n'.+1 then [seq b :: s | b <- [:: false; true], s <- sign_lists n']
  else [:: [::]].
Used by 3 declarations in 1 file
lemma size_sign_lists source, line 241 
forall n : nat, size (sign_lists n) = 2 ^ n
Statement as written in the source
Lemma size_sign_lists n : size (sign_lists n) = 2 ^ n.
Used by 1 declaration in 1 file
lemma mem_sign_lists source, line 246 
forall [n : nat] [s : seq bool], size s = n -> s \in sign_lists n
Statement as written in the source
Lemma mem_sign_lists n (s : seq bool) : size s = n -> s \in sign_lists n.
Used by 1 declaration in 1 file
lemma leq_ffact_expn source, line 252 
forall m n : nat, (m ^_ n <= m ^ n)%N
Statement as written in the source
Lemma leq_ffact_expn m n : (m ^_ n <= m ^ n)%N.
Used by 1 declaration in 1 file
sectionbinomial_bound
Variable R : realType.
lemma bin_le_expR main result source, line 265 
forall (R : realType) (m n : nat), ('C(m, n)%:R : R) <= ((expR 1 * m%:R / n%:R) ^+ n : R)

'C(m, n) <= (e m / n)^n.

Main result, as the README states it

C(m, n) <= (e m / n)^n. There are C(n + k, n) lists of n natural numbers with sum at most k.

Used in theories/ by: through net_exists
Statement as written in the source
Lemma bin_le_expR m n : ('C(m, n))%:R <= (expR 1 * m%:R / n%:R) ^+ n :> R.
Used by 1 declaration in 1 file
sectionnet_existence
Variable R : realType.
Implicit Types n : nat.
definition grid_point source, line 292
Type
forall {R : realType} {n : nat}, R -> seq nat * seq bool -> 'cV_n
Definition
Definition grid_point n (h : R) (c : seq nat * seq bool) : 'cV[R]_n :=
  \col_(i < n) ((-1) ^+ nth false c.2 i * (h * (nth 0%N c.1 i)%:R)).

The grid point of mesh h with code (a, s): its i-th coordinate is h * a_i, with the sign - if s_i holds.

Used by 4 declarations in 1 file
Arguments grid_point {n}.
definition grid_code source, line 298
Type
forall [R : realType] [n : nat], R -> 'cV_n -> seq nat * seq bool
Definition
Definition grid_code n (h : R) (x : 'cV[R]_n) : seq nat * seq bool :=
  ([seq Num.truncn (`|x i 0| / h) | i <- enum 'I_n],
   [seq x i 0 < 0 | i <- enum 'I_n]).

The code of x: the integer parts of the |x_i| / h and the signs of the x_i. Its grid point is within h of x in each coordinate.

Used by 5 declarations in 1 file
lemma grid_point_code source, line 302 
forall [R : realType] [n : nat] (h : R) (x : 'cV_n) (i : 'I_n),
grid_point h (grid_code h x) i 0 =
(-1) ^+ (x i 0 < 0)%R * (h * (Num.Def.truncn (`|x i 0| / h))%:R)
Statement as written in the source
Lemma grid_point_code n (h : R) (x : 'cV[R]_n) i :
  grid_point h (grid_code h x) i 0 =
    (-1) ^+ (x i 0 < 0)%R * (h * (Num.truncn (`|x i 0| / h))%:R).
Used by 1 declaration in 1 file
lemma grid_code_near source, line 310 
forall [R : realType] [n : nat] [h : R] (x : 'cV_n) (i : 'I_n),
0 < h -> `|x i 0 - grid_point h (grid_code h x) i 0| <= h
Statement as written in the source
Lemma grid_code_near n (h : R) (x : 'cV[R]_n) i :
  0 < h -> `|x i 0 - grid_point h (grid_code h x) i 0| <= h.
Used by 1 declaration in 1 file
lemma frobenius_col_sqr source, line 323 
forall [R : realType] [n : nat] (x : 'cV_n), frobenius x ^+ 2 = \sum_i x i 0 ^+ 2
Statement as written in the source
Lemma frobenius_col_sqr n (x : 'cV[R]_n) :
  frobenius x ^+ 2 = \sum_i x i 0 ^+ 2.
Used by 2 declarations in 1 file
lemma grid_code_dist source, line 329 
forall [R : realType] [n : nat] [h : R] (x : 'cV_n),
0 < h -> frobenius (x - grid_point h (grid_code h x)) ^+ 2 <= n%:R * h ^+ 2
Statement as written in the source
Lemma grid_code_dist n (h : R) (x : 'cV[R]_n) :
  0 < h -> frobenius (x - grid_point h (grid_code h x)) ^+ 2 <= n%:R * h ^+ 2.
Used by 1 declaration in 1 file
lemma sum_abs_col_le source, line 339 
forall [R : realType] [n : nat] (x : 'cV_n),
\sum_i `|x i 0| <= Num.ExtraDef.sqrtr n%:R * frobenius x
Statement as written in the source
Lemma sum_abs_col_le n (x : 'cV[R]_n) :
  \sum_i `|x i 0| <= Num.sqrt n%:R * frobenius x.
Used by 1 declaration in 1 file
definition grid_codes source, line 355
Type
nat -> nat -> seq (seq nat * seq bool)
Definition
Definition grid_codes n k : seq (seq nat * seq bool) :=
  [seq (a, s) | a <- budget n k, s <- sign_lists n].

The codes of the grid points: n naturals with sum at most k, and n signs.

Used by 3 declarations in 1 file
lemma size_grid_codes source, line 358 
forall n k : nat, size (grid_codes n k) = ('C(n + k, n) * 2 ^ n)%N
Statement as written in the source
Lemma size_grid_codes n k : size (grid_codes n k) = ('C(n + k, n) * 2 ^ n)%N.
Used by 1 declaration in 1 file
lemma grid_code_mem source, line 361 
forall [R : realType] [n k : nat] [h : R] [x : 'cV_n],
0 < h -> \sum_i `|x i 0| < k.+1%:R * h -> grid_code h x \in grid_codes n k
Statement as written in the source
Lemma grid_code_mem n k (h : R) (x : 'cV[R]_n) : 0 < h ->
  \sum_i `|x i 0| < k.+1%:R * h -> grid_code h x \in grid_codes n k.
Used by 1 declaration in 1 file
lemma grid_net source, line 375 
forall [R : realType] [n : nat] [S0 : set 'cV_n] [h eps : R] [k : nat],
0 < h ->
0 <= eps ->
n%:R * h ^+ 2 <= (eps / 2) ^+ 2 ->
(forall x : 'cV_n, S0 x -> \sum_i `|x i 0| < k.+1%:R * h) ->
exists N : seq 'cV_n,
  [/\ forall y : 'cV[R]_n, y \in N -> S0 y,
      is_net S0 N eps
    & (size N <= 'C(n + k, n) * 2 ^ n)%N]

A set whose points have small codes has a net of points of the set, one for each code.

Statement as written in the source
Lemma grid_net n (S : set 'cV[R]_n) (h eps : R) (k : nat) :
  0 < h -> 0 <= eps -> n%:R * h ^+ 2 <= (eps / 2) ^+ 2 ->
  (forall x, S x -> \sum_i `|x i 0| < k.+1%:R * h) ->
  exists N : seq 'cV[R]_n, [/\ forall y, y \in N -> S y, is_net S N eps &
    (size N <= 'C(n + k, n) * 2 ^ n)%N].
Used by 1 declaration in 1 file
lemma net_exists main result source, line 406 
forall [R : realType] [n : nat] [S0 : set 'cV_n] [r eps : R],
0 <= r ->
0 < eps ->
(forall x : 'cV_n, S0 x -> frobenius x <= r) ->
exists N : seq 'cV_n,
  [/\ forall y : 'cV[R]_n, y \in N -> S0 y,
      is_net S0 N eps
    & (size N)%:R <= (2 * expR 1 * (1 + 2 * r / eps)) ^+ n]

Every set in the ball of radius r has an eps-net of at most (2 e (1 + 2 r / eps))^n of its own points.

Main result, as the README states it

Every set in the ball of radius r of 'cV[R]_n has an eps-net of at most (2 e (1 + 2 r / eps))^n of its own points; for the unit ball and the unit sphere, r = 1. Proved by rounding to a grid of mesh eps / (2 sqrt n) and counting the grid points.

Used in theories/ by: Spectral/OperatorNet (unit_sphere_net); comparison/escape.v in the library
Statement as written in the source
Lemma net_exists n (S : set 'cV[R]_n) (r eps : R) : 0 <= r -> 0 < eps ->
  (forall x, S x -> frobenius x <= r) ->
  exists N : seq 'cV[R]_n, [/\ forall y, y \in N -> S y, is_net S N eps &
    (size N)%:R <= (2 * expR 1 * (1 + 2 * r / eps)) ^+ n].
Used by 9 declarations in 6 files
corollary unit_ball_net main result source, line 449 
forall [R : realType] (n : nat) [eps : R],
0 < eps ->
exists N : seq 'cV_n,
  [/\ forall y : 'cV[R]_n,
      y \in N -> frobenius y <= 1,
      is_net (unit_ball (n:=n)) N eps
    & (size N)%:R <= (2 * expR 1 * (1 + 2 / eps)) ^+ n]
Main result

Stated in the README together with net_exists.

Statement as written in the source
Corollary unit_ball_net n (eps : R) : 0 < eps ->
  exists N : seq 'cV[R]_n, [/\ forall y, y \in N -> frobenius y <= 1,
    is_net (@unit_ball R n) N eps &
    (size N)%:R <= (2 * expR 1 * (1 + 2 / eps)) ^+ n].
Used by 1 declaration in 1 file
corollary unit_sphere_net main result source, line 459 
forall [R : realType] (n : nat) [eps : R],
0 < eps ->
exists N : seq 'cV_n,
  [/\ forall y : 'cV[R]_n,
      y \in N -> frobenius y = 1,
      is_net (unit_sphere (n:=n)) N eps
    & (size N)%:R <= (2 * expR 1 * (1 + 2 / eps)) ^+ n]
Main result

Stated in the README together with net_exists.

Statement as written in the source
Corollary unit_sphere_net n (eps : R) : 0 < eps ->
  exists N : seq 'cV[R]_n, [/\ forall y, y \in N -> frobenius y = 1,
    is_net (@unit_sphere R n) N eps &
    (size N)%:R <= (2 * expR 1 * (1 + 2 / eps)) ^+ n].
Used by 2 declarations in 1 file
Arguments grid_point {R n}.
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.