GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisrandom_matrixgoe_entries

Tails of the entries of the GOE matrix

GaussianAnalysis.random_matrix.goe_entrieslibrary/random_matrix/goe_entries.v528 lines21 lemmas and theorems, 1 definitionsource
Imports 10 library modules and 26 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.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.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, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 1

For a of law gauss (d * d) and the GOE matrix W = goe_mx a of random_matrix/goe.v, each entry of W is a linear form of a: W_ij = <a, goe_coef i j> (goe_mx_mxdot). The coefficient vector of a diagonal entry has squared norm 2 / d (frobenius_goe_coef_diag), and the coefficient vectors of the entries of a row outside the diagonal are orthogonal, of squared norm 1 / d (mxdot_goe_coef_row). Hence, for s >= 0 and u > 0,

P(|W_ii| >= s) <= 2 exp (- d s^2 / 4)               (goe_mx_diag_tail),
P(|W_ij| >= s) <= 2 exp (- d s^2 / 2) if i != j  (goe_mx_offdiag_tail),
P(sum_(j != i) W_ij^2 >= 1 + u) <= exp (- d u^2 / (4 (1 + u))),

the last one (goe_mx_row_tail) because d sum_(j != i) W_ij^2 has the law of a chi-square with d - 1 degrees of freedom (gauss_mulmx_law, then gauss_centered_chi2_upper_tail of comparison/chi_square.v). Union bounds over the d diagonal entries, the d^2 entries and the d rows give the tails of the maxima, with the factors 2 d, 2 d^2 and d (goe_mx_diag_max_tail, goe_mx_offdiag_max_tail, goe_mx_row_max_tail); their events are measurable (measurable_goe_diag_max and the next two).

Three general facts are proved on the way: removing the diagonal of a square matrix A costs at most max_i |A_ii| in operator norm (opnorm_sub_diag_le, from opnorm_diag_mx_le); the union bound mu (\bigcup_i F i) <= \sum_i mu (F i) for a measure mu, a finite index type and measurable sets F i (measure_bigcup_fin_le); and x^k exp (- x c) <= 6 / (c^3 x) for c > 0, x >= 1 and k <= 2 (exprn_expRN_le), so that such tails, times at most d^2 events, are of order 1 / d.

Part of target T4 of phase 12: a Rocq formalization of the credited argument of the proof of the proposition 'Good disorder' (rcut:prop:good-disorder) of 'Cutoff throughout the high-temperature Sherrington-Kirkpatrick phase' (family 227 of the OpenAI math collection, revision 1581d4cbd, file appendices/entropy.tex), for the diagonal entries, the off-diagonal entries and the row sums of squares of the GOE matrix; the proposition itself belongs to target T4. It follows the TeX, not a Lean module of the collection. The manuscript bounds a row sum by the exponential Markov bound with E exp (theta (g^2 - 1)) <= exp (C theta^2) for |theta| <= 1/4; the chi-square tail used here has the same form with explicit constants.

goe_coef i jthe row vector c of 'rV[R]_(d * d) such that goe_mx a i j = <a, c> for every a

Main results

ResultsStatement
goe_mx_mxdotgoe_mx_diag_tailgoe_mx_offdiag_tailgoe_mx_row_tail
For a of law gauss (d * d) and the GOE matrix W = goe_mx a, every entry is a linear form of a: W_ij = <a, goe_coef i j>. For s >= 0: P(|W_ii| >= s) <= 2 exp (- d s^2 / 4), and P(|W_ij| >= s) <= 2 exp (- d s^2 / 2) if i != j. For u > 0 and every i: P(sum_(j != i) W_ij^2 >= 1 + u) <= exp (- d u^2 / (4 (1 + u))), since d sum_(j != i) W_ij^2 has the law of a chi-square with d - 1 degrees of freedom. A Rocq formalization of the credited argument of a proposition of family 227 of the OpenAI math collection (see the header).
goe_mx_diag_max_tailgoe_mx_offdiag_max_tailgoe_mx_row_max_tailmeasurable_goe_diag_maxmeasurable_goe_offdiag_maxmeasurable_goe_row_maxmeasurable_goe_opnorm_ge
Union bounds over the entries and the rows: for s >= 0 and u > 0, P(max_i |W_ii| >= s) <= 2 d exp (- d s^2 / 4), P(max_(i != j) |W_ij| >= s) <= 2 d^2 exp (- d s^2 / 2) and P(max_i sum_(j != i) W_ij^2 >= 1 + u) <= d exp (- d u^2 / (4 (1 + u))). These events, and {opnorm W >= c} for every real c, are measurable.
opnorm_sub_diag_leopnorm_diag_mx_lemeasure_bigcup_fin_leexprn_expRN_le
For a square matrix A and b >= 0 with |A_ii| <= b for every i: opnorm (A - diag A) <= opnorm A + b, because opnorm (diag_mx v) <= b when every |v_i| <= b. For a measure mu, a finite index type and measurable sets F i: mu (\bigcup_i F i) <= \sum_i mu (F i). For c > 0, x >= 1 and k <= 2: x^k exp (- x c) <= 6 / (c^3 x).

Declarations22 exported

lemma, theoremdefinitioninstancelocal
sectionopnorm_diag
Context {R : realType}.
lemma opnorm_diag_mx_le main result source, line 77 
forall {R : realType} [n : nat] [v : 'rV_n] [b : R],
0 <= b -> (forall i : 'I_n, `|v 0 i| <= b) -> opnorm (diag_mx v) <= b

The operator norm of a diagonal matrix is at most a bound of its entries.

Main result

Stated in the README together with opnorm_sub_diag_le.

Statement as written in the source
Lemma opnorm_diag_mx_le n (v : 'rV[R]_n) (b : R) : 0 <= b ->
  (forall i, `|v 0 i| <= b) -> opnorm (diag_mx v) <= b.
Used by 1 declaration in 1 file
lemma opnorm_sub_diag_le main result source, line 93 
forall {R : realType} [n : nat] [A : 'M_n] [b : R],
0 <= b ->
(forall i : 'I_n, `|A i i| <= b) -> opnorm (A - diag_mx (\row_i A i i)) <= opnorm A + b

Removing the diagonal of A costs at most a bound of its entries.

Main result, as the README states it

For a square matrix A and b >= 0 with |A_ii| <= b for every i: opnorm (A - diag A) <= opnorm A + b, because opnorm (diag_mx v) <= b when every |v_i| <= b. For a measure mu, a finite index type and measurable sets F i: mu (\bigcup_i F i) <= \sum_i mu (F i). For c > 0, x >= 1 and k <= 2: x^k exp (- x c) <= 6 / (c^3 x).

Statement as written in the source
Lemma opnorm_sub_diag_le n (A : 'M[R]_n) (b : R) : 0 <= b ->
  (forall i, `|A i i| <= b) ->
  opnorm (A - diag_mx (\row_i A i i)) <= opnorm A + b.
Used by 1 declaration in 1 file
sectionunion_bound
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
Local Open Scope ereal_scope.
lemma measure_bigcup_fin_le main result source, line 110 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  (mu : measure T R) [I : finType] [F : I -> set T],
(forall i : I, d.-measurable (F i)) -> (mu (\bigcup_i F i) <= (\sum_i mu (F i))%R)%E

The union bound for a family indexed by a finite type.

Main result

Stated in the README together with opnorm_sub_diag_le.

Statement as written in the source
Lemma measure_bigcup_fin_le (I : finType) (F : I -> set T) :
  (forall i, measurable (F i)) -> mu (\bigcup_i F i) <= \sum_i mu (F i).
Used by 3 declarations in 1 file
sectionexp_poly
Context {R : realType}.
lemma exprn_expRN_le main result source, line 129 
forall {R : realType} [c x : R] [k : nat],
0 < c -> 1 <= x -> (k <= 2)%N -> x ^+ k * expR (- (x * c)) <= 6 / c ^+ 3 / x

x^k exp (- x c) <= 6 / (c^3 x) for c > 0, x >= 1 and k <= 2.

Main result

Stated in the README together with opnorm_sub_diag_le.

Statement as written in the source
Lemma exprn_expRN_le (c x : R) (k : nat) : 0 < c -> 1 <= x -> (k <= 2)%N ->
  x ^+ k * expR (- (x * c)) <= 6 / c ^+ 3 / x.
Used by 1 declaration in 1 file
sectiongoe_entries
Context {R : realType} (d : nat).
definition goe_coef source, line 157
Type
forall {R : realType} [d : nat], 'I_d -> 'I_d -> 'rV_(d * d)
Definition
Definition goe_coef (i j : 'I_d) : 'rV[R]_(d * d) :=
  (Num.sqrt (2 * d%:R))^-1 *:
    (delta_mx 0 (mxvec_index i j) + delta_mx 0 (mxvec_index j i)).

The entry (i, j) of goe_mx a is the inner product of a with goe_coef i j.

Used by 6 declarations in 1 file
lemma goe_mx_mxdot main result source, line 161 
forall {R : realType} [d : nat] (a : 'rV_(d * d)) (i j : 'I_d),
goe_mx a i j = mxdot a (goe_coef i j)
Main result, as the README states it

For a of law gauss (d * d) and the GOE matrix W = goe_mx a, every entry is a linear form of a: W_ij = <a, goe_coef i j>. For s >= 0: P(|W_ii| >= s) <= 2 exp (- d s^2 / 4), and P(|W_ij| >= s) <= 2 exp (- d s^2 / 2) if i != j. For u > 0 and every i: P(sum_(j != i) W_ij^2 >= 1 + u) <= exp (- d u^2 / (4 (1 + u))), since d sum_(j != i) W_ij^2 has the law of a chi-square with d - 1 degrees of freedom. A Rocq formalization of the credited argument of a proposition of family 227 of the OpenAI math collection (see the header).

Statement as written in the source
Lemma goe_mx_mxdot (a : 'rV[R]_(d * d)) i j :
  goe_mx a i j = mxdot a (goe_coef i j).
Used by 3 declarations in 1 file
lemma delta_mxvec_index source, line 165 
forall {R : realType} [d : nat] (i j i' j' : 'I_d),
('e_(mxvec_index i j) : 'rV_(d * d)) 0 (mxvec_index i' j') = ((i' == i) && (j' == j))%:R
Statement as written in the source
Lemma delta_mxvec_index (i j i' j' : 'I_d) :
  (delta_mx 0 (mxvec_index i j) : 'rV[R]_(d * d)) 0 (mxvec_index i' j') =
  ((i' == i) && (j' == j))%:R.
Used by 2 declarations in 1 file
lemma mxdot_goe_coef_row source, line 175 
forall {R : realType} [d : nat] [i j j' : 'I_d],
j != i -> j' != i -> mxdot (goe_coef i j) (goe_coef i j') = (j == j')%:R / d%:R

Within the row i, the vectors goe_coef i j, j != i, are orthogonal, of squared norm 1 / d.

Statement as written in the source
Lemma mxdot_goe_coef_row (i j j' : 'I_d) : j != i -> j' != i ->
  mxdot (goe_coef i j) (goe_coef i j') = (j == j')%:R / d%:R.
Used by 2 declarations in 1 file
lemma frobenius_goe_coef_diag source, line 191 
forall {R : realType} [d : nat] (i : 'I_d), frobenius (goe_coef i i) ^+ 2 = 2 / d%:R
Statement as written in the source
Lemma frobenius_goe_coef_diag (i : 'I_d) :
  frobenius (goe_coef i i) ^+ 2 = 2 / d%:R.
Used by 1 declaration in 1 file
theorem goe_mx_diag_tail main result source, line 207 
forall {R : realType} [d : nat] (i : 'I_d) [s : R],
0 <= s ->
(gauss (d * d) [set a | (s <= `|goe_mx a i i|)%R] <= (2 * expR (- (d%:R * s ^+ 2 / 4)))%:E)%E

Gaussian tails of the entries, of variance 2 / d on the diagonal and 1 / d off the diagonal.

Main result

Stated in the README together with goe_mx_mxdot.

Statement as written in the source
Theorem goe_mx_diag_tail (i : 'I_d) (s : R) : 0 <= s ->
  (gauss (d * d) [set a | s <= `|goe_mx a i i|]%R <=
   (2 * expR (- (d%:R * s ^+ 2 / 4)))%:E)%E.
Used by 1 declaration in 1 file
theorem goe_mx_offdiag_tail main result source, line 226 
forall {R : realType} [d : nat] [i j : 'I_d] [s : R],
i != j ->
0 <= s ->
(gauss (d * d) [set a | (s <= `|goe_mx a i j|)%R] <= (2 * expR (- (d%:R * s ^+ 2 / 2)))%:E)%E
Main result

Stated in the README together with goe_mx_mxdot.

Statement as written in the source
Theorem goe_mx_offdiag_tail (i j : 'I_d) (s : R) : i != j -> 0 <= s ->
  (gauss (d * d) [set a | s <= `|goe_mx a i j|]%R <=
   (2 * expR (- (d%:R * s ^+ 2 / 2)))%:E)%E.
Used by 1 declaration in 1 file
theorem goe_mx_row_tail main result source, line 249 
forall {R : realType} [d : nat] (i : 'I_d) [u : R],
0 < u ->
(gauss (d * d) [set a | (1 + u <= \sum_(j | j != i) goe_mx a i j ^+ 2)%R] <=
 (expR (- (d%:R * u ^+ 2 / (4 * (1 + u)))))%:E)%E

The squares of the row i off the diagonal sum to 1 / d times a chi-square with d - 1 degrees of freedom: their tail above 1 + u.

Main result

Stated in the README together with goe_mx_mxdot.

Statement as written in the source
Theorem goe_mx_row_tail (i : 'I_d) (u : R) : 0 < u ->
  (gauss (d * d) [set a | 1 + u <= \sum_(j | j != i) goe_mx a i j ^+ 2]%R <=
   (expR (- (d%:R * u ^+ 2 / (4 * (1 + u)))))%:E)%E.
Used by 1 declaration in 1 file
lemma measurable_goe_entry source, line 355 
forall {R : realType} [d : nat] (i j : 'I_d),
measurable_fun [set: 'rV_(d * d)]
  (fun a : 'rV_(d * d) =>
   goe_mx a i j)
Statement as written in the source
Lemma measurable_goe_entry (i j : 'I_d) :
  measurable_fun [set: 'rV[R]_(d * d)] (fun a => goe_mx a i j).
Used by 2 declarations in 1 file
lemma measurable_goe_entry_ge source, line 361 
forall {R : realType} [d : nat] (i j : 'I_d) (c : R),
(measure_matrix_display default_measure_display).-measurable [set a | c <= `|goe_mx a i j|]
Statement as written in the source
Lemma measurable_goe_entry_ge (i j : 'I_d) (c : R) :
  measurable [set a : 'rV[R]_(d * d) | c <= `|goe_mx a i j|]%R.
Used by 4 declarations in 1 file
lemma measurable_goe_row_ge source, line 374 
forall {R : realType} [d : nat] (i : 'I_d) (c : R),
(measure_matrix_display default_measure_display).-measurable
  [set a | c <= \sum_(j | j != i) goe_mx a i j ^+ 2]
Statement as written in the source
Lemma measurable_goe_row_ge (i : 'I_d) (c : R) :
  measurable
    [set a : 'rV[R]_(d * d) | c <= \sum_(j | j != i) goe_mx a i j ^+ 2]%R.
Used by 2 declarations in 1 file
lemma measurable_goe_opnorm_ge main result source, line 393 
forall {R : realType} [d : nat] (c : R),
(measure_matrix_display default_measure_display).-measurable
  [set a | c <= opnorm (goe_mx a)]
Main result

Stated in the README together with goe_mx_diag_max_tail.

Statement as written in the source
Lemma measurable_goe_opnorm_ge (c : R) :
  measurable [set a : 'rV[R]_(d * d) | c <= opnorm (goe_mx a)]%R.
Used by 1 declaration in 1 file
lemma measurable_goe_diag_max main result source, line 417 
forall {R : realType} [d : nat] (s : R),
(measure_matrix_display default_measure_display).-measurable
  [set a | (exists i : 'I_d, s <= `|goe_mx a i i|)]

The events of the three maxima below are measurable.

Main result

Stated in the README together with goe_mx_diag_max_tail.

Statement as written in the source
Lemma measurable_goe_diag_max (s : R) :
  measurable [set a : 'rV[R]_(d * d) | exists i, s <= `|goe_mx a i i|]%R.
Used by 1 declaration in 1 file
lemma measurable_goe_offdiag_max main result source, line 429 
forall {R : realType} [d : nat] (s : R),
(measure_matrix_display default_measure_display).-measurable
  [set a | (exists i j : 'I_d,
              i != j /\ s <= `|goe_mx a i j|)]
Main result

Stated in the README together with goe_mx_diag_max_tail.

Statement as written in the source
Lemma measurable_goe_offdiag_max (s : R) :
  measurable [set a : 'rV[R]_(d * d) |
    exists i j, i != j /\ s <= `|goe_mx a i j|]%R.
Used by 1 declaration in 1 file
lemma measurable_goe_row_max main result source, line 445 
forall {R : realType} [d : nat] (c : R),
(measure_matrix_display default_measure_display).-measurable
  [set a | (exists i : 'I_d,
              c <= \sum_(j | j != i) goe_mx a i j ^+ 2)]
Main result

Stated in the README together with goe_mx_diag_max_tail.

Statement as written in the source
Lemma measurable_goe_row_max (c : R) :
  measurable [set a : 'rV[R]_(d * d) |
    exists i, c <= \sum_(j | j != i) goe_mx a i j ^+ 2]%R.
Used by 1 declaration in 1 file
theorem goe_mx_diag_max_tail main result source, line 461 
forall {R : realType} (d : nat) [s : R],
0 <= s ->
(gauss (d * d) [set a | (exists i : 'I_d, (s <= `|goe_mx a i i|)%R)] <=
 (2 * d%:R * expR (- (d%:R * s ^+ 2 / 4)))%:E)%E

The largest diagonal entry, the largest entry off the diagonal and the largest row sum of squares off the diagonal, by the union bound.

Main result, as the README states it

Union bounds over the entries and the rows: for s >= 0 and u > 0, P(max_i |W_ii| >= s) <= 2 d exp (- d s^2 / 4), P(max_(i != j) |W_ij| >= s) <= 2 d^2 exp (- d s^2 / 2) and P(max_i sum_(j != i) W_ij^2 >= 1 + u) <= d exp (- d u^2 / (4 (1 + u))). These events, and {opnorm W >= c} for every real c, are measurable.

Statement as written in the source
Theorem goe_mx_diag_max_tail (s : R) : 0 <= s ->
  (gauss (d * d) [set a | exists i, s <= `|goe_mx a i i|]%R <=
   (2 * d%:R * expR (- (d%:R * s ^+ 2 / 4)))%:E)%E.
Used by 1 declaration in 1 file
theorem goe_mx_offdiag_max_tail main result source, line 480 
forall {R : realType} (d : nat) [s : R],
0 <= s ->
(gauss (d * d)
   [set a | (exists i j : 'I_d,
               i != j /\ (s <= `|goe_mx a i j|)%R)] <=
 (2 * d%:R ^+ 2 * expR (- (d%:R * s ^+ 2 / 2)))%:E)%E
Main result

Stated in the README together with goe_mx_diag_max_tail.

Statement as written in the source
Theorem goe_mx_offdiag_max_tail (s : R) : 0 <= s ->
  (gauss (d * d)
     [set a | exists i j, i != j /\ s <= `|goe_mx a i j|]%R <=
   (2 * d%:R ^+ 2 * expR (- (d%:R * s ^+ 2 / 2)))%:E)%E.
Used by 1 declaration in 1 file
theorem goe_mx_row_max_tail main result source, line 507 
forall {R : realType} (d : nat) [u : R],
0 < u ->
(gauss (d * d)
   [set a | (exists i : 'I_d,
               (1 + u <= \sum_(j | j != i) goe_mx a i j ^+ 2)%R)] <=
 (d%:R * expR (- (d%:R * u ^+ 2 / (4 * (1 + u)))))%:E)%E
Main result

Stated in the README together with goe_mx_diag_max_tail.

Statement as written in the source
Theorem goe_mx_row_max_tail (u : R) : 0 < u ->
  (gauss (d * d)
     [set a | exists i, 1 + u <= \sum_(j | j != i) goe_mx a i j ^+ 2]%R <=
   (d%:R * expR (- (d%:R * u ^+ 2 / (4 * (1 + u)))))%:E)%E.
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.