GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysismatrixtensor_packing

Tensor packing

GaussianAnalysis.matrix.tensor_packinglibrary/matrix/tensor_packing.v1,214 lines50 lemmas and theorems, 4 definitionssource
Imports 11 library modules and 27 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.classical.functions, mathcomp.algebra.interval, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.exp, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.numfun, mathcomp.analysis.measurable_realfun, mathcomp.analysis.probability_theory.probability

Imported by 1

Rows x_1, ..., x_m in the unit ball of 'rV[R]_n1 and y_1, ..., y_m in the unit ball of 'rV[R]_n2 are almost orthogonal: |<x_a, x_b>| <= eta and |<y_a, y_b>| <= eta for a != b outside two relations Gx and Gy with at most L successors at every vertex. Then few of the tensors x_a^T y_a of 'M[R]_(n1, n2), with the Frobenius inner product, have a large projection on a subspace of small dimension: if A_1, ..., A_r are Frobenius-orthonormal with r <= d, 0 < eps <= 1, d >= 1 and 0 <= eta <= eps^2 / 10^4, then at most

30000 (1 + L) / eps^2 exp (30000 sqrt d ln (2 + d) / eps^2)

indices a have sum_k (x_a A_k y_a^T)^2 >= eps^2, the left side being the squared norm of the projection of x_a^T y_a on the span of the A_k.

This file is a Rocq formalization of the credited argument of Theorem 4.1, 'Tensor packing', of 'Pointwise convergence of fourfold ergodic averages for mixing transformations' (OpenAI, 4 October 2026), family 154 of the OpenAI math collection at revision 1581d4cbd (sections/04-packing.tex). The same theorem is in the section 'Tensor packing' of its companion 'Pointwise Multiple Ergodic Averages for Mixing Transformations'. There is no Lean version. The proof is the manuscript's:

  • the spectral subspaces E_1 of \sum_k A_k A_k^T and E_2 of \sum_k A_k^T A_k for the eigenvalues larger than sqrt d have dimension at most sqrt d, since both traces are r <= d;
  • few indices a have a projection of x_a on E_1, or of y_a on E_2, of norm larger than eps / 10: cover these projections by balls of radius eps / 40 and apply the cluster bound to each ball;
  • for the other indices, the coefficients v_a of x_a^T y_a on the compressions B_k = Q_1 A_k Q_2, where Q_i projects on the orthogonal complement of E_i, have norm at least 4 eps / 5, so the clusters around a maximal eps / 8-separated set J of them have at most 3 (1 + L) / eps^2 indices each;
  • Sudakov's minoration (comparison/sudakov.v) bounds sqrt (ln #|J|) by a multiple of E opnorm (\sum_k g_k B_k) / eps, and the Gaussian matrix series bound gauss_mx_series_opnorm_log of random_matrix/matrix_series.v bounds this expectation by 5 d^(1/4) sqrt (ln (2 + d)), since \sum_k B_k B_k^T and \sum_k B_k^T B_k have operator norm at most sqrt d and trace at most d.

The formalization differs from the manuscript in four points:

  • the dimensions are finite, and the projection of rank at most d is given by an orthonormal basis A_1, ..., A_r of its range; the reduction from Hilbert spaces to finite spans and the consequence for d_m = (1 + log m)^(3/2) are not formalized;
  • the relations need not be symmetric, and their degree is the number of successors;
  • the clusters of the remaining indices use the relation Gx alone, with |<x_a^T y_a, x_b^T y_b>| = |<x_a, x_b>| |<y_a, y_b>| <= eta, where the manuscript uses the union of the two graphs and eta^2;
  • the constant is explicit, C = 30000, and the coverings are those of net_exists (matrix/nets.v), with (2 e (1 + 80 / eps))^k balls in dimension k where the manuscript has (1 + 80 / eps)^k.

Proved:

  • almost_orthogonal_sum_le, the cluster bound: if <v_a, v_a> <= 1 and |<v_a, v_b>| <= eta for a != b outside a relation with at most L successors, then |\sum_(a in S) v_a|^2 <= (1 + L) |S| + eta |S|^2; almost_orthogonal_card_le: if moreover |\sum_(a in S) v_a| >= rho |S| with rho >= 0 and rho^2 > eta, then |S| <= (1 + L) / (rho^2 - eta).
  • large_projection_card: for such columns X_a in the unit ball and V with orthonormal rows (V V^T = 1) in 'M[R]_(k, n), at most (2 e (1 + 80 / eps))^k 200 (1 + L) / eps^2 indices have |V X_a| > eps / 10, when 0 <= eta <= eps^2 / 10^4.
  • bessel_mxdot, Bessel's inequality: \sum_k <Z, A_k>^2 <= <Z, Z> for a Frobenius-orthonormal family, so the coefficient map mxcoef A is a contraction (frobenius_mxcoef_le).
  • maximal_separated_subset: every finite set I of indices has a delta-separated subset J such that every point of I is at distance less than delta of a point of J.
  • spectral_rowperp_form_le: for P orthogonal and t >= 0, the quadratic form of P^T diag(e) P on the range of rowperp V, where V = select_rows P [set u | t < e_u], is at most t |z|^2.
  • opnorm_compress_gram, trace_compress_gram: if the quadratic form of \sum_k A_k A_k^T on the range of rowperp V1 is at most t |z|^2, with t >= 0, then the compressions B_k = rowperp V1 A_k rowperp V2 satisfy opnorm (\sum_k B_k B_k^T) <= t and tr (\sum_k B_k B_k^T) <= \sum_k |A_k|^2.
  • sudakov_mx_series: if the coefficient vectors on B_1, ..., B_r of the tensors x_i^T y_i of l + 1 pairs of rows in the unit balls are delta-separated, then for g of law gauss r, delta (sqrt (ln (l + 1)) / 2 - 2) <= sqrt 2 E opnorm (\sum_k g_k B_k).
  • tensor_packing: the theorem, with the constant 30000.
select_rows P Sthe rows of P indexed by the set S, a matrix with #|S| rows
rowproj VV^T V, the orthogonal projection on the span of the rows of V when V V^T = 1
rowperp V1 - V^T V
mxcoef A Zthe row of the inner products <Z, A_k>, k < r

Main results

ResultsStatement
tensor_packing
Tensor packing (Theorem 4.1 of 'Pointwise convergence of fourfold ergodic averages for mixing transformations', family 154 of the OpenAI math collection): for rows x_1, ..., x_m and y_1, ..., y_m in the unit balls of 'rV[R]_n1 and 'rV[R]_n2, relations Gx and Gy on 'I_m with at most L successors at every vertex that contain every pair a != b with |<x_a, x_b>| > eta (respectively |<y_a, y_b>| > eta), Frobenius-orthonormal A_1, ..., A_r in 'M[R]_(n1, n2) with r <= d, 0 < eps <= 1, d >= 1 and 0 <= eta <= eps^2 / 10^4, at most 30000 (1 + L) / eps^2 exp (30000 sqrt d ln (2 + d) / eps^2) indices a have sum_k (x_a A_k y_a^T)^2 >= eps^2. Proved by cutting the spectra of sum_k A_k A_k^T and sum_k A_k^T A_k at sqrt d, Sudakov's minoration and gauss_mx_series_opnorm_log.
almost_orthogonal_sum_lealmost_orthogonal_card_lelarge_projection_card
Almost orthogonal families: if eta >= 0, <v_a, v_a> <= 1 and |<v_a, v_b>| <= eta for a != b outside a relation with at most L successors at every vertex, then |sum_(a in S) v_a|^2 <= (1 + L) s + eta s^2 with s = #|S|, so a set S with |sum_(a in S) v_a| >= rho s, rho >= 0 and rho^2 > eta has at most (1 + L) / (rho^2 - eta) elements. For such columns X_a in the unit ball of 'cV[R]_n, V in 'M[R]_(k, n) with V V^T = 1, eps > 0 and 0 <= eta <= eps^2 / 10^4, at most (2 e (1 + 80 / eps))^k 200 (1 + L) / eps^2 indices have |V X_a| > eps / 10.
bessel_mxdotmxcoeffrobenius_mxcoef_lemaximal_separated_subsetcard_le_cover
Bessel's inequality sum_k <Z, A_k>^2 <= <Z, Z> for a Frobenius-orthonormal family, so mxcoef A Z, the row of the <Z, A_k>, is a contraction. Every finite set I of indices has a subset J whose points v_b are pairwise at distance at least delta > 0 and such that every point of I is at distance less than delta from a point of J. A set covered by sets C_b, b in J, of at most B elements each has at most #|J| B elements.
select_rowsrowprojrowperpspectral_rowperp_form_leopnorm_compress_gramtrace_compress_gram
select_rows P S is the matrix of the rows of P indexed by S, with orthonormal rows when P is orthogonal; rowproj V = V^T V and rowperp V = 1 - V^T V are complementary orthogonal projections when V V^T = 1. For P orthogonal, t >= 0 and V = select_rows P [set u | t < e_u], the quadratic form of P^T diag(e) P on the range of rowperp V is at most t |z|^2. If this bound holds for sum_k A_k A_k^T and V1, the compressions B_k = rowperp V1 A_k rowperp V2 satisfy opnorm (sum_k B_k B_k^T) <= t and tr (sum_k B_k B_k^T) <= sum_k |A_k|_F^2.
sudakov_mx_seriesseparated_card_sudakov
Sudakov's minoration for a Gaussian matrix series: if the coefficient vectors mxcoef B (x_i^T y_i) of l + 1 tensors of rows in the unit balls are pairwise at distance at least delta >= 0, then delta (sqrt (ln (l + 1)) / 2 - 2) <= sqrt 2 E opnorm (sum_k g_k B_k) for g of law gauss r; likewise with ln #|J| for a separated set J of indices.

Declarations54 exported

lemma, theoremdefinitioninstancelocal
sectionfrobenius_sum
Context {R : realType} {p q : nat}.
lemma frobenius_sum_le source, line 122 
forall {R : realType} {p q : nat} [I : finType] (P : pred I) (F : I -> 'M_(p, q)),
frobenius (\sum_(i | P i) F i) <= \sum_(i | P i) frobenius (F i)

The triangle inequality for finite sums.

Statement as written in the source
Lemma frobenius_sum_le (I : finType) (P : pred I) (F : I -> 'M[R]_(p, q)) :
  frobenius (\sum_(i | P i) F i) <= \sum_(i | P i) frobenius (F i).
Used by 2 declarations in 1 file
sectionalmost_orthogonal
Context {R : realType} {m p q : nat}.
lemma almost_orthogonal_sum_le main result source, line 138 
forall {R : realType} {m p q : nat} [v : 'I_m -> 'M_(p, q)] [G : rel 'I_m] 
  [L : nat] [eta : R] (S0 : {set 'I_m}),
0 <= eta ->
(forall a : 'I_m, mxdot (v a) (v a) <= 1) ->
(forall a : 'I_m, (#|[set b | G a b]| <= L)%N) ->
(forall a b : 'I_m,
 a != b -> ~~ G a b -> `|mxdot (v a) (v b)| <= eta) ->
mxdot (\sum_(a in S0) v a) (\sum_(a in S0) v a) <=
(1 + L%:R) * #|S0|%:R + eta * #|S0|%:R ^+ 2

The cluster bound: unit vectors whose inner products are at most eta outside a relation of out-degree at most L have, on every set S, |\sum_(a in S) v a|^2 <= (1 + L) |S| + eta |S|^2.

Main result, as the README states it

Almost orthogonal families: if eta >= 0, <v_a, v_a> <= 1 and |<v_a, v_b>| <= eta for a != b outside a relation with at most L successors at every vertex, then |sum_(a in S) v_a|^2 <= (1 + L) s + eta s^2 with s = #|S|, so a set S with |sum_(a in S) v_a| >= rho s, rho >= 0 and rho^2 > eta has at most (1 + L) / (rho^2 - eta) elements. For such columns X_a in the unit ball of 'cV[R]_n, V in 'M[R]_(k, n) with V V^T = 1, eps > 0 and 0 <= eta <= eps^2 / 10^4, at most (2 e (1 + 80 / eps))^k 200 (1 + L) / eps^2 indices have |V X_a| > eps / 10.

Statement as written in the source
Lemma almost_orthogonal_sum_le (v : 'I_m -> 'M[R]_(p, q)) (G : rel 'I_m)
    (L : nat) (eta : R) (S : {set 'I_m}) :
  0 <= eta -> (forall a, mxdot (v a) (v a) <= 1) ->
  (forall a, #|[set b | G a b]| <= L)%N ->
  (forall a b, a != b -> ~~ G a b -> `|mxdot (v a) (v b)| <= eta) ->
  mxdot (\sum_(a in S) v a) (\sum_(a in S) v a) <=
    (1 + L%:R) * #|S|%:R + eta * #|S|%:R ^+ 2.
Used by 2 declarations in 1 file
sectionalmost_orthogonal_card
Context {R : realType} {m p q : nat}.
Variables (T : 'I_m -> 'M[R]_(p, q)) (G : rel 'I_m) (L : nat) (eta : R).
Hypothesis eta0 : 0 <= eta.
Hypothesis T1 : forall a, mxdot (T a) (T a) <= 1.
Hypothesis deg : forall a, (#|[set b | G a b]| <= L)%N.
Hypothesis ex : forall a b, a != b -> ~~ G a b -> `|mxdot (T a) (T b)| <= eta.
lemma almost_orthogonal_card_le main result source, line 186 
forall {R : realType} {m p q : nat} [T : 'I_m -> 'M_(p, q)] [G : rel 'I_m] 
  [L : nat] [eta : R],
0 <= eta ->
(forall a : 'I_m, mxdot (T a) (T a) <= 1) ->
(forall a : 'I_m, (#|[set b | G a b]| <= L)%N) ->
(forall a b : 'I_m,
 a != b -> ~~ G a b -> `|mxdot (T a) (T b)| <= eta) ->
forall [C : {set 'I_m}] [rho : R],
0 <= rho ->
eta < rho ^+ 2 ->
rho * #|C|%:R <= frobenius (\sum_(a in C) T a) -> #|C|%:R <= (1 + L%:R) / (rho ^+ 2 - eta)

A set whose sum has norm at least rho times its size, with rho^2 > eta, has at most (1 + L) / (rho^2 - eta) elements.

Main result

Stated in the README together with almost_orthogonal_sum_le.

Statement as written in the source
Lemma almost_orthogonal_card_le (C : {set 'I_m}) (rho : R) :
  0 <= rho -> eta < rho ^+ 2 ->
  rho * #|C|%:R <= frobenius (\sum_(a in C) T a) ->
  #|C|%:R <= (1 + L%:R) / (rho ^+ 2 - eta).
Used by 1 declaration in 1 file
sectionbessel
Context {R : realType} {p q r : nat}.
lemma bessel_mxdot main result source, line 212 
forall {R : realType} {p q r : nat} [A : 'I_r -> 'M_(p, q)] (Z : 'M_(p, q)),
(forall k l : 'I_r, mxdot (A k) (A l) = (k == l)%:R) ->
\sum_k mxdot Z (A k) ^+ 2 <= mxdot Z Z

Bessel's inequality for a Frobenius-orthonormal family.

Main result, as the README states it

Bessel's inequality sum_k <Z, A_k>^2 <= <Z, Z> for a Frobenius-orthonormal family, so mxcoef A Z, the row of the <Z, A_k>, is a contraction. Every finite set I of indices has a subset J whose points v_b are pairwise at distance at least delta > 0 and such that every point of I is at distance less than delta from a point of J. A set covered by sets C_b, b in J, of at most B elements each has at most #|J| B elements.

Statement as written in the source
Lemma bessel_mxdot (A : 'I_r -> 'M[R]_(p, q)) (Z : 'M[R]_(p, q)) :
  (forall k l, mxdot (A k) (A l) = (k == l)%:R) ->
  \sum_k mxdot Z (A k) ^+ 2 <= mxdot Z Z.
Used by 1 declaration in 1 file
sectionisometry
Context {R : realType} {k n : nat}.
Variable V : 'M[R]_(k, n).
Hypothesis VV : V *m V^T = 1%:M.
lemma frobenius_trmx_isometry source, line 237 
forall {R : realType} {k n : nat} [V : 'M_(k, n)],
V *m V^T = 1%:M -> forall w : 'cV_k, frobenius (V^T *m w) = frobenius w

For V with orthonormal rows, V^T is an isometry and V a contraction.

Statement as written in the source
Lemma frobenius_trmx_isometry (w : 'cV[R]_k) :
  frobenius (V^T *m w) = frobenius w.
Used by 1 declaration in 1 file
lemma frobenius_isometry_le source, line 244 
forall {R : realType} {k n : nat} [V : 'M_(k, n)],
V *m V^T = 1%:M -> forall z : 'cV_n, frobenius (V *m z) <= frobenius z
Statement as written in the source
Lemma frobenius_isometry_le (z : 'cV[R]_n) : frobenius (V *m z) <= frobenius z.
Used by 2 declarations in 1 file
sectionlarge_projection
Context {R : realType} {k n m : nat}.
Variables (V : 'M[R]_(k, n)) (X : 'I_m -> 'cV[R]_n) (G : rel 'I_m).
Variables (L : nat) (eta eps : R).
Hypothesis VV : V *m V^T = 1%:M.
Hypothesis eps0 : 0 < eps.
Hypothesis eta0 : 0 <= eta.
Hypothesis eta_eps : eta <= eps ^+ 2 / 10000.
Hypothesis X1 : forall a, frobenius (X a) <= 1.
Hypothesis deg : forall a, (#|[set b | G a b]| <= L)%N.
Hypothesis ex : forall a b, a != b -> ~~ G a b -> `|mxdot (X a) (X b)| <= eta.
lemma large_projection_cluster_card source, line 271 
forall {R : realType} {k n m : nat} [V : 'M_(k, n)] [X : 'I_m -> 'cV_n] 
  [G : rel 'I_m] [L : nat] [eta eps : R],
V *m V^T = 1%:M ->
0 < eps ->
0 <= eta ->
eta <= eps ^+ 2 / 10000 ->
(forall a : 'I_m, frobenius (X a) <= 1) ->
(forall a : 'I_m, (#|[set b | G a b]| <= L)%N) ->
(forall a b : 'I_m,
 a != b -> ~~ G a b -> `|mxdot (X a) (X b)| <= eta) ->
forall [y : 'cV_k] [C : {set 'I_m}],
eps / 10 < frobenius y ->
(forall a : 'I_m, a \in C -> frobenius (V *m X a - y) <= eps / 40) ->
#|C|%:R <= 200 * (1 + L%:R) / eps ^+ 2

A cluster of vectors whose images under V are within eps / 40 of a point of norm larger than eps / 10 has at most 200 (1 + L) / eps^2 elements.

Statement as written in the source
Lemma large_projection_cluster_card (y : 'cV[R]_k) (C : {set 'I_m}) :
  eps / 10 < frobenius y ->
  (forall a, a \in C -> frobenius (V *m X a - y) <= eps / 40) ->
  #|C|%:R <= 200 * (1 + L%:R) / eps ^+ 2.
Used by 1 declaration in 1 file
lemma large_projection_card main result source, line 315 
forall {R : realType} {k n m : nat} [V : 'M_(k, n)] [X : 'I_m -> 'cV_n] 
  [G : rel 'I_m] [L : nat] [eta eps : R],
V *m V^T = 1%:M ->
0 < eps ->
0 <= eta ->
eta <= eps ^+ 2 / 10000 ->
(forall a : 'I_m, frobenius (X a) <= 1) ->
(forall a : 'I_m, (#|[set b | G a b]| <= L)%N) ->
(forall a b : 'I_m,
 a != b -> ~~ G a b -> `|mxdot (X a) (X b)| <= eta) ->
#|[set a | eps / 10 < frobenius (V *m X a)]|%:R <=
(2 * expR 1 * (1 + 80 / eps)) ^+ k * (200 * (1 + L%:R) / eps ^+ 2)

The number of vectors whose image under V has norm larger than eps / 10 is at most (2 e (1 + 80 / eps))^k 200 (1 + L) / eps^2: cover the images, in the unit ball of 'cV[R]_k, by balls of radius eps / 40.

Main result

Stated in the README together with almost_orthogonal_sum_le.

Statement as written in the source
Lemma large_projection_card :
  #|[set a | eps / 10 < frobenius (V *m X a)]|%:R <=
  (2 * expR 1 * (1 + 80 / eps)) ^+ k * (200 * (1 + L%:R) / eps ^+ 2).
Used by 1 declaration in 1 file
sectionmaximal_separated
Context {R : realType} {m r : nat}.
Variables (v : 'I_m -> 'rV[R]_r) (delta : R).
Hypothesis delta0 : 0 < delta.
lemma maximal_separated_subset main result source, line 367 
forall {R : realType} {m r : nat} (v : 'I_m -> 'rV_r) [delta : R],
0 < delta ->
forall I : {set 'I_m},
exists J : {set 'I_m},
  [/\ J \subset I,
      forall a b : 'I_m, a \in J -> b \in J -> a != b -> delta <= frobenius (v a - v b)
    & forall a : 'I_m, a \in I -> exists2 b : 'I_m, b \in J & frobenius (v a - v b) < delta]

A maximal delta-separated subset J of a finite set I of indices: the points v b, b in J, are pairwise at distance at least delta, and every point v a, a in I, is at distance less than delta of one of them.

Main result

Stated in the README together with bessel_mxdot.

Statement as written in the source
Lemma maximal_separated_subset (I : {set 'I_m}) : exists J : {set 'I_m},
  [/\ J \subset I,
      forall a b, a \in J -> b \in J -> a != b -> delta <= frobenius (v a - v b)
    & forall a, a \in I -> exists2 b, b \in J & frobenius (v a - v b) < delta].
Used by 1 declaration in 1 file
sectioncover_count
Context {R : realType} {m : nat}.
lemma card_le_cover main result source, line 412 
forall {R : realType} {m : nat} [I J : {set 'I_m}] [C : 'I_m -> {set 'I_m}] [B : R],
(forall a : 'I_m, a \in I -> exists2 b : 'I_m, b \in J & a \in C b) ->
(forall b : 'I_m, b \in J -> #|C b|%:R <= B) -> #|I|%:R <= #|J|%:R * B

A set covered by clusters C b, b in J, of at most B elements each has at most #|J| B elements.

Main result

Stated in the README together with bessel_mxdot.

Statement as written in the source
Lemma card_le_cover (I J : {set 'I_m}) (C : 'I_m -> {set 'I_m}) (B : R) :
  (forall a, a \in I -> exists2 b, b \in J & a \in C b) ->
  (forall b, b \in J -> #|C b|%:R <= B) ->
  #|I|%:R <= #|J|%:R * B.
Used by 1 declaration in 1 file
sectionselect_rows
Context {R : realType} {n : nat}.
Variables (P : 'M[R]_n) (A : {set 'I_n}).
Hypothesis Po : P \is orthogonalmx.
definition select_rows main result source, line 442
Type
forall {R : realType} {n : nat}, 'M_n -> forall A : {set 'I_n}, 'M_(#|A|, n)
Definition
Definition select_rows : 'M[R]_(#|A|, n) := \matrix_(i, j) P (enum_val i) j.

The rows of P indexed by A, an orthonormal family.

Main result, as the README states it

select_rows P S is the matrix of the rows of P indexed by S, with orthonormal rows when P is orthogonal; rowproj V = V^T V and rowperp V = 1 - V^T V are complementary orthogonal projections when V V^T = 1. For P orthogonal, t >= 0 and V = select_rows P [set u | t < e_u], the quadratic form of P^T diag(e) P on the range of rowperp V is at most t |z|^2. If this bound holds for sum_k A_k A_k^T and V1, the compressions B_k = rowperp V1 A_k rowperp V2 satisfy opnorm (sum_k B_k B_k^T) <= t and tr (sum_k B_k B_k^T) <= sum_k |A_k|_F^2.

Used by 5 declarations in 1 file
lemma select_rows_orth source, line 444 
forall {R : realType} {n : nat} [P : 'M_n] (A : {set 'I_n}),
P \is orthogonalmx -> select_rows P A *m (select_rows P A)^T = 1%:M
Statement as written in the source
Lemma select_rows_orth : select_rows *m select_rows^T = 1%:M.
Used by 1 declaration in 1 file
lemma select_rows_proj source, line 454 
forall {R : realType} {n : nat} (P : 'M_n) (A : {set 'I_n}),
(select_rows P A)^T *m select_rows P A =
P^T *m diag_mx (\row_u (if u \in A then 1 else 0)) *m P
Statement as written in the source
Lemma select_rows_proj : select_rows^T *m select_rows =
  P^T *m diag_mx (\row_u (if u \in A then 1 else 0)) *m P.
Used by 1 declaration in 1 file
sectionrowproj
Context {R : realType} {k n : nat}.
Variable V : 'M[R]_(k, n).
Hypothesis VV : V *m V^T = 1%:M.
definition rowproj main result source, line 474
Type
forall {R : realType} {k n : nat}, 'M_(k, n) -> 'M_n
Definition
Definition rowproj : 'M[R]_n := V^T *m V.

The orthogonal projection V^T V onto the span of the rows of V, and the projection onto its orthogonal complement.

Main result

Stated in the README together with select_rows.

Used by 9 declarations in 1 file
definition rowperp main result source, line 475
Type
forall {R : realType} {k n : nat}, 'M_(k, n) -> 'M_n
Definition
Definition rowperp : 'M[R]_n := 1%:M - rowproj.
Main result

Stated in the README together with select_rows.

Used by 12 declarations in 1 file
lemma rowprojT source, line 477 
forall {R : realType} {k n : nat} (V : 'M_(k, n)), (rowproj V)^T = rowproj V
Statement as written in the source
Lemma rowprojT : rowproj^T = rowproj.
Used by 3 declarations in 1 file
lemma rowperpT source, line 480 
forall {R : realType} {k n : nat} (V : 'M_(k, n)), (rowperp V)^T = rowperp V
Statement as written in the source
Lemma rowperpT : rowperp^T = rowperp.
Used by 4 declarations in 1 file
lemma rowprojK source, line 483 
forall {R : realType} {k n : nat} [V : 'M_(k, n)],
V *m V^T = 1%:M -> rowproj V *m rowproj V = rowproj V
Statement as written in the source
Lemma rowprojK : rowproj *m rowproj = rowproj.
Used by 1 declaration in 1 file
lemma rowproj_perp source, line 486 
forall {R : realType} {k n : nat} [V : 'M_(k, n)],
V *m V^T = 1%:M -> rowproj V *m rowperp V = 0
Statement as written in the source
Lemma rowproj_perp : rowproj *m rowperp = 0.
Used by 2 declarations in 1 file
lemma rowperpK source, line 489 
forall {R : realType} {k n : nat} [V : 'M_(k, n)],
V *m V^T = 1%:M -> rowperp V *m rowperp V = rowperp V
Statement as written in the source
Lemma rowperpK : rowperp *m rowperp = rowperp.
lemma mxdot_rowproj_perp source, line 494 
forall {R : realType} {k n : nat} [V : 'M_(k, n)],
V *m V^T = 1%:M ->
forall [p : nat] (Z : 'M_(n, p)), mxdot (rowproj V *m Z) (rowperp V *m Z) = 0
Statement as written in the source
Lemma mxdot_rowproj_perp p (Z : 'M[R]_(n, p)) :
  mxdot (rowproj *m Z) (rowperp *m Z) = 0.
Used by 1 declaration in 1 file
lemma frobenius_rowperp_le source, line 501 
forall {R : realType} {k n : nat} [V : 'M_(k, n)],
V *m V^T = 1%:M ->
forall [p : nat] (Z : 'M_(n, p)), frobenius (rowperp V *m Z) <= frobenius Z
Statement as written in the source
Lemma frobenius_rowperp_le p (Z : 'M[R]_(n, p)) :
  frobenius (rowperp *m Z) <= frobenius Z.
Used by 4 declarations in 1 file
lemma frobenius_rowproj source, line 513 
forall {R : realType} {k n : nat} [V : 'M_(k, n)],
V *m V^T = 1%:M ->
forall [p : nat] (Z : 'M_(n, p)), frobenius (rowproj V *m Z) = frobenius (V *m Z)
Statement as written in the source
Lemma frobenius_rowproj p (Z : 'M[R]_(n, p)) :
  frobenius (rowproj *m Z) = frobenius (V *m Z).
Used by 1 declaration in 1 file
sectionspectral_rowperp
Context {R : realType} {n : nat}.
Variables (P : 'M[R]_n) (e : 'rV[R]_n) (t : R).
Hypothesis Po : P \is orthogonalmx.
Hypothesis t0 : 0 <= t.
Local Notation S := [set u | t < e 0 u].
Local Notation V := (select_rows P S).
lemma spectral_rowperp_coord source, line 533 
forall {R : realType} {n : nat} [P : 'M_n] (e : 'rV_n) (t : R),
P \is orthogonalmx ->
forall (z : 'cV_n) (u : 'I_n),
(P *m (rowperp (select_rows P [set u0 | t < e 0 u0]) *m z)) u 0 =
(if u \in [set u0 | t < e 0 u0] then 0 else (P *m z) u 0)

For V the rows of P of the eigenvalues e_u > t, rowperp V removes the coordinates of these eigenvalues in the basis of the rows of P.

Statement as written in the source
Lemma spectral_rowperp_coord (z : 'cV[R]_n) u :
  (P *m (rowperp V *m z)) u 0 = if u \in S then 0 else (P *m z) u 0.
Used by 1 declaration in 1 file
lemma spectral_rowperp_form_le main result source, line 544 
forall {R : realType} {n : nat} [P : 'M_n] (e : 'rV_n) [t : R],
P \is orthogonalmx ->
0 <= t ->
forall z : 'cV_n,
mxdot (rowperp (select_rows P [set u | t < e 0 u]) *m z)
  (P^T *m diag_mx e *m P *m (rowperp (select_rows P [set u | t < e 0 u]) *m z)) <=
t * mxdot z z

So the quadratic form of P^T diag(e) P on the range of rowperp V is at most t.

Main result

Stated in the README together with select_rows.

Statement as written in the source
Lemma spectral_rowperp_form_le (z : 'cV[R]_n) :
  mxdot (rowperp V *m z) ((P^T *m diag_mx e *m P) *m (rowperp V *m z)) <=
  t * mxdot z z.
Used by 1 declaration in 1 file
sectiongram
Context {R : realType} {n1 n2 r : nat}.
Variable A : 'I_r -> 'M[R]_(n1, n2).
lemma gram_form source, line 565 
forall {R : realType} {n1 n2 r : nat} (A : 'I_r -> 'M_(n1, n2)) (z : 'cV_n1),
mxdot z ((\sum_k A k *m (A k)^T) *m z) = \sum_k mxdot ((A k)^T *m z) ((A k)^T *m z)

The matrix \sum_k A_k A_k^T: its quadratic form is \sum_k |A_k^T z|^2, its trace \sum_k |A_k|^2, so r for an orthonormal family, and it is symmetric and positive semidefinite.

Statement as written in the source
Lemma gram_form (z : 'cV[R]_n1) :
  mxdot z ((\sum_k A k *m (A k)^T) *m z) =
  \sum_k mxdot ((A k)^T *m z) ((A k)^T *m z).
Used by 2 declarations in 1 file
lemma gram_trace source, line 573 
forall {R : realType} {n1 n2 r : nat} (A : 'I_r -> 'M_(n1, n2)),
\tr (\sum_k A k *m (A k)^T) = \sum_k mxdot (A k) (A k)
Statement as written in the source
Lemma gram_trace : \tr (\sum_k A k *m (A k)^T) = \sum_k mxdot (A k) (A k).
Used by 3 declarations in 1 file
lemma gram_sym source, line 576 
forall {R : realType} {n1 n2 r : nat} (A : 'I_r -> 'M_(n1, n2)),
\sum_k A k *m (A k)^T \is symmetricmx
Statement as written in the source
Lemma gram_sym : \sum_k A k *m (A k)^T \is symmetricmx.
Used by 1 declaration in 1 file
lemma gram_form_ge0 source, line 582 
forall {R : realType} {n1 n2 r : nat} (A : 'I_r -> 'M_(n1, n2)) (z : 'cV_n1),
0 <= mxdot z ((\sum_k A k *m (A k)^T) *m z)
Statement as written in the source
Lemma gram_form_ge0 (z : 'cV[R]_n1) :
  0 <= mxdot z ((\sum_k A k *m (A k)^T) *m z).
Used by 1 declaration in 1 file
lemma gram_trace_on source, line 586 
forall {R : realType} {n1 n2 r : nat} [A : 'I_r -> 'M_(n1, n2)],
(forall k l : 'I_r, mxdot (A k) (A l) = (k == l)%:R) -> \tr (\sum_k A k *m (A k)^T) = r%:R
Statement as written in the source
Lemma gram_trace_on : (forall k l, mxdot (A k) (A l) = (k == l)%:R) ->
  \tr (\sum_k A k *m (A k)^T) = r%:R.
Used by 1 declaration in 1 file
sectioncard_large
Context {R : realType} {n : nat}.
lemma card_large_le source, line 600 
forall {R : realType} {n : nat} [e : 'rV_n] (t : R),
(forall u : 'I_n, 0 <= e 0 u) -> #|[set u | t < e 0 u]|%:R * t <= \sum_u e 0 u

At most (\sum_u e_u) / t of the nonnegative e_u exceed t.

Statement as written in the source
Lemma card_large_le (e : 'rV[R]_n) (t : R) : (forall u, 0 <= e 0 u) ->
  #|[set u | t < e 0 u]|%:R * t <= \sum_u e 0 u.
Used by 1 declaration in 1 file
sectiontensor_rows
Context {R : realType} {n1 n2 : nat}.
lemma mxdot_tensor source, line 617 
forall {R : realType} {n1 n2 : nat} (x x' : 'rV_n1) (y y' : 'rV_n2),
mxdot (x^T *m y) (x'^T *m y') = mxdot x x' * mxdot y y'

The tensor x^T y of two rows: <x^T y, x'^T y'> = <x, x'> <y, y'>, and <x^T y, A> is the bilinear form x A y^T.

Statement as written in the source
Lemma mxdot_tensor (x x' : 'rV[R]_n1) (y y' : 'rV[R]_n2) :
  mxdot (x^T *m y) (x'^T *m y') = mxdot x x' * mxdot y y'.
Used by 2 declarations in 1 file
lemma frobenius_tensor source, line 624 
forall {R : realType} {n1 n2 : nat} (x : 'rV_n1) (y : 'rV_n2),
frobenius (x^T *m y) = frobenius x * frobenius y
Statement as written in the source
Lemma frobenius_tensor (x : 'rV[R]_n1) (y : 'rV[R]_n2) :
  frobenius (x^T *m y) = frobenius x * frobenius y.
Used by 1 declaration in 1 file
lemma mxdot_tensor_form source, line 630 
forall {R : realType} {n1 n2 : nat} (x : 'rV_n1) (y : 'rV_n2) (A : 'M_(n1, n2)),
mxdot (x^T *m y) A = (x *m A *m y^T) 0 0
Statement as written in the source
Lemma mxdot_tensor_form (x : 'rV[R]_n1) (y : 'rV[R]_n2) (A : 'M[R]_(n1, n2)) :
  mxdot (x^T *m y) A = (x *m A *m y^T) 0 0.
Used by 2 declarations in 1 file
sectionmxcoef
Context {R : realType} {p q r : nat}.
Variable A : 'I_r -> 'M[R]_(p, q).
Hypothesis Aon : forall k l, mxdot (A k) (A l) = (k == l)%:R.
definition mxcoef main result source, line 645
Type
forall {R : realType} {p q r : nat}, ('I_r -> 'M_(p, q)) -> 'M_(p, q) -> 'rV_r
Definition
Definition mxcoef (Z : 'M[R]_(p, q)) : 'rV[R]_r := \row_k mxdot Z (A k).

The coefficients of a matrix on the family A, its inner products with the A_k; a contraction when the family is orthonormal.

Main result

Stated in the README together with bessel_mxdot.

Used by 9 declarations in 1 file
lemma mxcoefD source, line 647 
forall {R : realType} {p q r : nat} (A : 'I_r -> 'M_(p, q))
  (Z Z' : 'M[R]_(p, q)),
mxcoef A (Z + Z') = mxcoef A Z + mxcoef A Z'
Statement as written in the source
Lemma mxcoefD Z Z' : mxcoef (Z + Z') = mxcoef Z + mxcoef Z'.
lemma mxcoefB source, line 650 
forall {R : realType} {p q r : nat} (A : 'I_r -> 'M_(p, q))
  (Z Z' : 'M[R]_(p, q)),
mxcoef A (Z - Z') = mxcoef A Z - mxcoef A Z'
Statement as written in the source
Lemma mxcoefB Z Z' : mxcoef (Z - Z') = mxcoef Z - mxcoef Z'.
Used by 1 declaration in 1 file
lemma mxcoef_sum source, line 653 
forall {R : realType} {p q r : nat} (A : 'I_r -> 'M_(p, q)) [I : finType] 
  (P : pred I) (F : I -> 'M_(p, q)),
mxcoef A (\sum_(i | P i) F i) = \sum_(i | P i) mxcoef A (F i)
Statement as written in the source
Lemma mxcoef_sum (I : finType) (P : pred I) (F : I -> 'M[R]_(p, q)) :
  mxcoef (\sum_(i | P i) F i) = \sum_(i | P i) mxcoef (F i).
Used by 1 declaration in 1 file
lemma frobenius_mxcoef_sqr source, line 660 
forall {R : realType} {p q r : nat} (A : 'I_r -> 'M_(p, q)) (Z : 'M_(p, q)),
frobenius (mxcoef A Z) ^+ 2 = \sum_k mxdot Z (A k) ^+ 2
Statement as written in the source
Lemma frobenius_mxcoef_sqr Z :
  frobenius (mxcoef Z) ^+ 2 = \sum_k mxdot Z (A k) ^+ 2.
Used by 2 declarations in 1 file
lemma frobenius_mxcoef_le main result source, line 667 
forall {R : realType} {p q r : nat} [A : 'I_r -> 'M_(p, q)],
(forall k l : 'I_r, mxdot (A k) (A l) = (k == l)%:R) ->
forall Z : 'M_(p, q), frobenius (mxcoef A Z) <= frobenius Z
Main result

Stated in the README together with bessel_mxdot.

Statement as written in the source
Lemma frobenius_mxcoef_le Z : frobenius (mxcoef Z) <= frobenius Z.
Used by 2 declarations in 1 file
sectioncompress_gram
Context {R : realType} {n1 n2 r k1 k2 : nat}.
Variable A : 'I_r -> 'M[R]_(n1, n2).
Variables (V1 : 'M[R]_(k1, n1)) (V2 : 'M[R]_(k2, n2)).
Variable t : R.
Hypothesis V1V1 : V1 *m V1^T = 1%:M.
Hypothesis V2V2 : V2 *m V2^T = 1%:M.
Hypothesis t0 : 0 <= t.
Hypothesis cut1 : forall z : 'cV[R]_n1,
  mxdot (rowperp V1 *m z) ((\sum_k A k *m (A k)^T) *m (rowperp V1 *m z)) <=
  t * mxdot z z.
lemma opnorm_compress_gram main result source, line 689 
forall {R : realType} {n1 n2 r k1 k2 : nat} [A : 'I_r -> 'M_(n1, n2)] 
  [V1 : 'M_(k1, n1)] [V2 : 'M_(k2, n2)] [t : R],
V2 *m V2^T = 1%:M ->
0 <= t ->
(forall z : 'cV_n1,
 mxdot (rowperp V1 *m z) ((\sum_k A k *m (A k)^T) *m (rowperp V1 *m z)) <= t * mxdot z z) ->
opnorm (\sum_k rowperp V1 *m A k *m rowperp V2 *m (rowperp V1 *m A k *m rowperp V2)^T) <= t

The compressions rowperp V1 A_k rowperp V2 inherit the bound t of the quadratic form on the range of rowperp V1, and the trace bound.

Main result

Stated in the README together with select_rows.

Statement as written in the source
Lemma opnorm_compress_gram :
  opnorm (\sum_k (rowperp V1 *m A k *m rowperp V2) *m
                 (rowperp V1 *m A k *m rowperp V2)^T) <= t.
Used by 1 declaration in 1 file
lemma trace_compress_gram main result source, line 707 
forall {R : realType} {n1 n2 r k1 k2 : nat} (A : 'I_r -> 'M_(n1, n2)) 
  [V1 : 'M_(k1, n1)] [V2 : 'M_(k2, n2)],
V1 *m V1^T = 1%:M ->
V2 *m V2^T = 1%:M ->
\tr (\sum_k rowperp V1 *m A k *m rowperp V2 *m (rowperp V1 *m A k *m rowperp V2)^T) <=
\sum_k mxdot (A k) (A k)
Main result

Stated in the README together with select_rows.

Statement as written in the source
Lemma trace_compress_gram :
  \tr (\sum_k (rowperp V1 *m A k *m rowperp V2) *m
              (rowperp V1 *m A k *m rowperp V2)^T) <=
  \sum_k mxdot (A k) (A k).
Used by 1 declaration in 1 file
sectioncompress
Context {R : realType} {n1 n2 r k1 k2 : nat}.
Variable A : 'I_r -> 'M[R]_(n1, n2).
Variables (V1 : 'M[R]_(k1, n1)) (V2 : 'M[R]_(k2, n2)).
Hypothesis Aon : forall k l, mxdot (A k) (A l) = (k == l)%:R.
Hypothesis V1V1 : V1 *m V1^T = 1%:M.
Hypothesis V2V2 : V2 *m V2^T = 1%:M.
lemma frobenius_outer source, line 730 
forall {R : realType} [m n : nat] (c : 'cV_m) (w : 'rV_n),
frobenius (c *m w) = frobenius c * frobenius w
Statement as written in the source
Lemma frobenius_outer m n (c : 'cV[R]_m) (w : 'rV[R]_n) :
  frobenius (c *m w) = frobenius c * frobenius w.
Used by 1 declaration in 1 file
lemma frobenius_rowperp_compress_le source, line 735 
forall {R : realType} {n1 n2 k1 k2 : nat} [V1 : 'M_(k1, n1)] [V2 : 'M_(k2, n2)],
V1 *m V1^T = 1%:M ->
V2 *m V2^T = 1%:M ->
forall Z : 'M_(n1, n2), frobenius (rowperp V1 *m Z *m rowperp V2) <= frobenius Z

Compressing by projections does not increase the Frobenius norm.

Statement as written in the source
Lemma frobenius_rowperp_compress_le (Z : 'M[R]_(n1, n2)) :
  frobenius (rowperp V1 *m Z *m rowperp V2) <= frobenius Z.
Used by 1 declaration in 1 file
lemma mxcoef_compress_near source, line 745 
forall {R : realType} {n1 n2 r k1 k2 : nat} [A : 'I_r -> 'M_(n1, n2)] 
  [V1 : 'M_(k1, n1)] [V2 : 'M_(k2, n2)],
(forall k l : 'I_r, mxdot (A k) (A l) = (k == l)%:R) ->
V1 *m V1^T = 1%:M ->
V2 *m V2^T = 1%:M ->
forall [x : 'rV_n1] [y : 'rV_n2] [eps : R],
frobenius x <= 1 ->
frobenius y <= 1 ->
frobenius (V1 *m x^T) <= eps ->
frobenius (V2 *m y^T) <= eps ->
frobenius (mxcoef A (x^T *m y) - mxcoef A (rowperp V1 *m (x^T *m y) *m rowperp V2)) <=
2 * eps

If the projections of x and y on the rows of V1 and V2 are small, then the coefficients of x^T y and of its compression are close.

Statement as written in the source
Lemma mxcoef_compress_near (x : 'rV[R]_n1) (y : 'rV[R]_n2) (eps : R) :
  frobenius x <= 1 -> frobenius y <= 1 ->
  frobenius (V1 *m x^T) <= eps -> frobenius (V2 *m y^T) <= eps ->
  frobenius (mxcoef A (x^T *m y) -
             mxcoef A (rowperp V1 *m (x^T *m y) *m rowperp V2)) <= 2 * eps.
Used by 1 declaration in 1 file
sectionsum_near
Context {R : realType} {m p q : nat}.
lemma frobenius_sum_near source, line 781 
forall {R : realType} {m p q : nat} [u : 'I_m -> 'M_(p, q)] [w : 'M_(p, q)]
  [C : {set 'I_m}] [delta : R],
(forall a : 'I_m, a \in C -> frobenius (u a - w) <= delta) ->
(frobenius w - delta) * #|C|%:R <= frobenius (\sum_(a in C) u a)

Points within delta of a center w have a sum of norm at least (|w| - delta) times their number.

Statement as written in the source
Lemma frobenius_sum_near (u : 'I_m -> 'M[R]_(p, q)) (w : 'M[R]_(p, q))
    (C : {set 'I_m}) (delta : R) :
  (forall a, a \in C -> frobenius (u a - w) <= delta) ->
  (frobenius w - delta) * #|C|%:R <= frobenius (\sum_(a in C) u a).
Used by 1 declaration in 1 file
sectionsudakov_mx_series
Context {R : realType} {n1 n2 r : nat}.
Variable B : 'I_r -> 'M[R]_(n1, n2).
lemma sudakov_mx_series main result source, line 808 
forall {R : realType} {n1 n2 r : nat} [B : 'I_r -> 'M_(n1, n2)] 
  [l : nat] [x : 'I_l.+1 -> 'rV_n1] [y : 'I_l.+1 -> 'rV_n2] [delta : R],
0 <= delta ->
(forall i : 'I_l.+1, frobenius (x i) <= 1) ->
(forall i : 'I_l.+1, frobenius (y i) <= 1) ->
(forall i j : 'I_l.+1,
 i != j -> delta <= frobenius (mxcoef B ((x i)^T *m y i) - mxcoef B ((x j)^T *m y j))) ->
delta * (Num.ExtraDef.sqrtr (ln l.+1%:R) / 2 - 2) <=
Num.ExtraDef.sqrtr 2 * \int[gauss r]_g opnorm (\sum_k g 0 k *: B k)

Sudakov's minoration for the coefficient vectors of x_i^T y_i on B: if they are delta-separated, then E opnorm (\sum_k g_k B_k) is at least delta (sqrt (ln (l + 1)) / 2 - 2) / sqrt 2.

Main result, as the README states it

Sudakov's minoration for a Gaussian matrix series: if the coefficient vectors mxcoef B (x_i^T y_i) of l + 1 tensors of rows in the unit balls are pairwise at distance at least delta >= 0, then delta (sqrt (ln (l + 1)) / 2 - 2) <= sqrt 2 E opnorm (sum_k g_k B_k) for g of law gauss r; likewise with ln #|J| for a separated set J of indices.

Statement as written in the source
Lemma sudakov_mx_series l (x : 'I_l.+1 -> 'rV[R]_n1) (y : 'I_l.+1 -> 'rV[R]_n2)
    (delta : R) :
  0 <= delta -> (forall i, frobenius (x i) <= 1) ->
  (forall i, frobenius (y i) <= 1) ->
  (forall i j, i != j ->
    delta <= frobenius (mxcoef B ((x i)^T *m y i) -
                        mxcoef B ((x j)^T *m y j))) ->
  delta * (Num.sqrt (ln l.+1%:R) / 2 - 2) <=
  Num.sqrt 2 * \int[gauss r]_g opnorm (\sum_k g 0 k *: B k).
Used by 1 declaration in 1 file
sectionseparated_card
Context {R : realType} {n1 n2 r m : nat}.
Variables (B : 'I_r -> 'M[R]_(n1, n2)) (x : 'I_m -> 'rV[R]_n1).
Variables (y : 'I_m -> 'rV[R]_n2).
Hypothesis x1 : forall a, frobenius (x a) <= 1.
Hypothesis y1 : forall a, frobenius (y a) <= 1.
lemma separated_card_sudakov main result source, line 854 
forall {R : realType} {n1 n2 r m : nat} [B : 'I_r -> 'M_(n1, n2)] 
  [x : 'I_m -> 'rV_n1] [y : 'I_m -> 'rV_n2],
(forall a : 'I_m, frobenius (x a) <= 1) ->
(forall a : 'I_m, frobenius (y a) <= 1) ->
forall [J : {set 'I_m}] [delta M : R],
0 <= delta ->
(forall a b : 'I_m,
 a \in J ->
 b \in J ->
 a != b -> delta <= frobenius (mxcoef B ((x a)^T *m y a) - mxcoef B ((x b)^T *m y b))) ->
\int[gauss r]_g opnorm (\sum_k g 0 k *: B k) <= M ->
delta * (Num.ExtraDef.sqrtr (ln #|J|%:R) / 2 - 2) <= Num.ExtraDef.sqrtr 2 * M
Main result

Stated in the README together with sudakov_mx_series.

Statement as written in the source
Lemma separated_card_sudakov (J : {set 'I_m}) (delta M : R) : 0 <= delta ->
  (forall a b, a \in J -> b \in J -> a != b ->
    delta <= frobenius (mxcoef B ((x a)^T *m y a) -
                        mxcoef B ((x b)^T *m y b))) ->
  \int[gauss r]_g opnorm (\sum_k g 0 k *: B k) <= M ->
  delta * (Num.sqrt (ln #|J|%:R) / 2 - 2) <= Num.sqrt 2 * M.
Used by 1 declaration in 1 file
sectionpacking_arith
Context {R : realType}.
lemma ln_le_subr1 source, line 887 
forall {R : realType} [u : R], 0 < u -> ln u <= u - 1

ln u <= u - 1 for u > 0.

Statement as written in the source
Lemma ln_le_subr1 (u : R) : 0 < u -> ln u <= u - 1.
Used by 1 declaration in 1 file
lemma tensor_packing_net source, line 894 
forall {R : realType} [eps d : R] [k : nat],
0 < eps ->
eps <= 1 ->
1 <= d ->
k%:R <= Num.ExtraDef.sqrtr d ->
(2 * expR 1 * (1 + 80 / eps)) ^+ k <=
expR (972 * Num.ExtraDef.sqrtr d * ln (2 + d) / eps ^+ 2)

The number of balls covering the discarded projections, for a dimension k <= sqrt d.

Statement as written in the source
Lemma tensor_packing_net (eps d : R) (k : nat) :
  0 < eps -> eps <= 1 -> 1 <= d ->
  k%:R <= Num.sqrt d ->
  (2 * expR 1 * (1 + 80 / eps)) ^+ k <=
  expR (972 * Num.sqrt d * ln (2 + d) / eps ^+ 2).
Used by 1 declaration in 1 file
lemma tensor_packing_separated source, line 930 
forall {R : realType} [eps d : R] [l : nat],
0 < eps ->
eps <= 1 ->
1 <= d ->
eps / 8 * (Num.ExtraDef.sqrtr (ln l%:R) / 2 - 2) <=
Num.ExtraDef.sqrtr 2 * (5 * d `^ 4^-1 * Num.ExtraDef.sqrtr (ln (2 + d))) ->
l%:R <= expR (25648 * Num.ExtraDef.sqrtr d * ln (2 + d) / eps ^+ 2)

The size l of the separated set, from Sudakov's minoration and the bound 5 d^(1/4) sqrt (ln (2 + d)) of the expected operator norm.

Statement as written in the source
Lemma tensor_packing_separated (eps d : R) (l : nat) :
  0 < eps -> eps <= 1 -> 1 <= d ->
  eps / 8 * (Num.sqrt (ln l%:R) / 2 - 2) <=
    Num.sqrt 2 * (5 * d `^ 4^-1 * Num.sqrt (ln (2 + d))) ->
  l%:R <= expR (25648 * Num.sqrt d * ln (2 + d) / eps ^+ 2).
Used by 1 declaration in 1 file
lemma tensor_packing_cluster source, line 990 
forall {R : realType} [eps eta u : R],
0 < eps ->
0 <= eta ->
eta <= eps ^+ 2 / 10000 -> 0 <= u -> u / ((27 * eps / 40) ^+ 2 - eta) <= 3 * (u / eps ^+ 2)

The size of the clusters of the remaining indices, for rho = 27 eps / 40.

Statement as written in the source
Lemma tensor_packing_cluster (eps eta u : R) : 0 < eps -> 0 <= eta ->
  eta <= eps ^+ 2 / 10000 -> 0 <= u ->
  u / ((27 * eps / 40) ^+ 2 - eta) <= 3 * (u / eps ^+ 2).
Used by 1 declaration in 1 file
lemma tensor_packing_count source, line 1005 
forall {R : realType} [N D1 D2 I J K1 K2 F Q X : R],
0 <= F ->
0 <= X ->
0 <= J ->
0 <= Q ->
N <= D1 + D2 + I ->
D1 <= K1 * (200 * F) ->
D2 <= K2 * (200 * F) ->
I <= J * Q ->
K1 <= expR (972 * X) ->
K2 <= expR (972 * X) ->
J <= expR (25648 * X) -> Q <= 3 * F -> N <= 30000 * F * expR (30000 * X)

The final count: the discarded indices and the clusters around the separated set.

Statement as written in the source
Lemma tensor_packing_count (N D1 D2 I J K1 K2 F Q X : R) :
  0 <= F -> 0 <= X -> 0 <= J -> 0 <= Q ->
  N <= D1 + D2 + I ->
  D1 <= K1 * (200 * F) -> D2 <= K2 * (200 * F) -> I <= J * Q ->
  K1 <= expR (972 * X) -> K2 <= expR (972 * X) -> J <= expR (25648 * X) ->
  Q <= 3 * F ->
  N <= 30000 * F * expR (30000 * X).
Used by 1 declaration in 1 file
sectiontensor_packing
Context {R : realType}.
Local Notation gauss := (@gauss R).
theorem tensor_packing main result source, line 1037 
forall {R : realType} [m n1 n2 r d L : nat] [eps eta : R] [x : 'I_m -> 'rV_n1]
  [y : 'I_m -> 'rV_n2] [Gx Gy : rel 'I_m] [A : 'I_r -> 'M_(n1, n2)],
0 < eps ->
eps <= 1 ->
(0 < d)%N ->
0 <= eta ->
eta <= eps ^+ 2 / 10000 ->
(forall a : 'I_m, frobenius (x a) <= 1) ->
(forall a : 'I_m, frobenius (y a) <= 1) ->
(forall a : 'I_m, (#|[set b | Gx a b]| <= L)%N) ->
(forall a : 'I_m, (#|[set b | Gy a b]| <= L)%N) ->
(forall a b : 'I_m,
 a != b -> eta < `|mxdot (x a) (x b)| -> Gx a b) ->
(forall a b : 'I_m,
 a != b -> eta < `|mxdot (y a) (y b)| -> Gy a b) ->
(forall k l : 'I_r, mxdot (A k) (A l) = (k == l)%:R) ->
(r <= d)%N ->
#|[set a | eps ^+ 2 <= \sum_k (x a *m A k *m (y a)^T) 0 0 ^+ 2]|%:R <=
30000 * (1 + L%:R) / eps ^+ 2 *
expR (30000 * Num.ExtraDef.sqrtr d%:R * ln (2 + d%:R) / eps ^+ 2)

Tensor packing (Theorem 4.1 of the fourfold paper of family 154), with the constant 30000.

Main result, as the README states it

Tensor packing (Theorem 4.1 of 'Pointwise convergence of fourfold ergodic averages for mixing transformations', family 154 of the OpenAI math collection): for rows x_1, ..., x_m and y_1, ..., y_m in the unit balls of 'rV[R]_n1 and 'rV[R]_n2, relations Gx and Gy on 'I_m with at most L successors at every vertex that contain every pair a != b with |<x_a, x_b>| > eta (respectively |<y_a, y_b>| > eta), Frobenius-orthonormal A_1, ..., A_r in 'M[R]_(n1, n2) with r <= d, 0 < eps <= 1, d >= 1 and 0 <= eta <= eps^2 / 10^4, at most 30000 (1 + L) / eps^2 exp (30000 sqrt d ln (2 + d) / eps^2) indices a have sum_k (x_a A_k y_a^T)^2 >= eps^2. Proved by cutting the spectra of sum_k A_k A_k^T and sum_k A_k^T A_k at sqrt d, Sudakov's minoration and gauss_mx_series_opnorm_log.

Statement as written in the source
Theorem tensor_packing (m n1 n2 r d L : nat) (eps eta : R)
    (x : 'I_m -> 'rV[R]_n1) (y : 'I_m -> 'rV[R]_n2) (Gx Gy : rel 'I_m)
    (A : 'I_r -> 'M[R]_(n1, n2)) :
  0 < eps -> eps <= 1 -> (0 < d)%N -> 0 <= eta -> eta <= eps ^+ 2 / 10000 ->
  (forall a, frobenius (x a) <= 1) -> (forall a, frobenius (y a) <= 1) ->
  (forall a, #|[set b | Gx a b]| <= L)%N ->
  (forall a, #|[set b | Gy a b]| <= L)%N ->
  (forall a b, a != b -> eta < `|mxdot (x a) (x b)| -> Gx a b) ->
  (forall a b, a != b -> eta < `|mxdot (y a) (y b)| -> Gy a b) ->
  (forall k l, mxdot (A k) (A l) = (k == l)%:R) -> (r <= d)%N ->
  #|[set a | eps ^+ 2 <= \sum_k ((x a) *m A k *m (y a)^T) 0 0 ^+ 2]|%:R <=
  30000 * (1 + L%:R) / eps ^+ 2 *
    expR (30000 * Num.sqrt d%:R * ln (2 + d%:R) / eps ^+ 2).
Used by 1 declaration in 1 file
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.