On this page

The Gaussian orthogonal ensemble

GaussianAnalysis.random_matrix.goelibrary/random_matrix/goe.v1,256 lines71 lemmas and theorems, 6 definitionssource

Imports 12 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 9

Required by 6 files of the paper proofs

For a of law gauss (d * d), goe_mx a is the symmetric matrix W = (A + A^T) / sqrt (2 d) with A = vec_mx a: the entries W_ij, i <= j, are independent centered normal with variance 1 / d off the diagonal and 2 / d on it. This normalization has the semicircle law of radius 2 (semicircle_prob 2 of probability/semicircle_law.v) as limit of its spectrum. The Gaussian features of Koehler and Sohn at kappa = 3 (arXiv 2608.27372, lines 1004-1086) have the same law up to mxvec. This file is part of item G7 of phase 5.

Proved:

polyfun F: F is continuous on 'rV[R]_m and of polynomial growth, the hypothesis of Gaussian integration by parts (gauss_ibp); it holds for constants and coordinates and is stable under sums and products (polyfunD, polyfunM, polyfun_sum), hence for the entries of sums, products and powers of matrices with such entries (mx_polyfun) and for their traces.
is_derive_mxpow: the derivative of M |-> (M ^+ k) i j at W along E is the entry (i, j) of mxpow_deriv W E k = \sum_(r < k) W^r E W^(k-1-r); mxpow_deriv_trace: for W symmetric, \sum_(i, j) of the entries (j, i) of mxpow_deriv W (E_ij + E_ji) k is k tr W^(k-1) + \sum_(r < k) tr W^r tr W^(k-1-r).
gauss_ibp_polyfun: Gaussian integration by parts E[x_p F x] = E[d_p F x] for F and d_p F of polynomial growth.
goe_schwinger_dyson: the Schwinger-Dyson equation for the moments of W, E tr W^(k+1) = (k E tr W^(k-1) + \sum_(r < k) E[tr W^r tr W^(k-1-r)]) / d, by integration by parts in each coordinate a_ij of a; with t_k = tr W^k / d it reads E t_(k+1) = (k / d) E t_(k-1) + \sum_(r < k) E[t_r t_(k-1-r)].
The operator norm: frobenius W <= sqrt (2 / d) |a| (frobenius_goe_mx), so opnorm W is sqrt (2 / d)-Lipschitz in a (goe_opnorm_lipschitz); E opnorm W <= 2 sqrt 2 for d >= 1 (goe_opnorm_mean, from gauss_opnorm_mean and E |g| <= sqrt n, gauss_frobenius_mean); and E exp (s opnorm W) <= exp (2 sqrt 2 s + s^2 / d) for s >= 0 (goe_opnorm_mgf, by Gaussian concentration).
goe_tr_var: with t_k = goe_tr k = tr W^k / d, for every u >= 0, Var t_k <= 2 L^2 + 8 (2k)! exp (2 sqrt 2 (2u + 1) + (2u + 1)^2 / d - 6u) with L = sqrt 2 k 3^(k-1) / d. The statistic goe_clip k of the eigenvalues clipped to [-3, 3] is L-Lipschitz in a (goe_clip_lipschitz, by the Hoffman-Wielandt inequality), so its variance is at most L^2 (gauss_poincare_lipschitz), and |t_k - goe_clip k| <= 2 opnorm W^k exp (u (opnorm W - 3)) (goe_clip_err). With u = sqrt d, Var t_k tends to 0: goe_tr_var_small, Var t_k <= eps for every large d.
goe_tr_sd: E t_(k+2) = (k + 1) / d E t_k + \sum_(r <= k) E[t_r t_(k-r)], and Rintegral_cov_le: |Cov (X, Y)| <= (Var X + Var Y) / 2.
goe_opnorm_tail_small: for c > 2 sqrt 2 and eps > 0, P(opnorm W >= c) <= eps for every large d, from gauss_tail_expR (Markov's inequality for exp (s F)) and goe_opnorm_mgf.

The convergence of E t_k to the moments of the semicircle law and Wigner's law are in wigner.v (goe_moment_cvg, wigner).

`goe_mx a`	the GOE matrix (A + A^T) / sqrt (2 d) of a row vector a of size d * d, A = vec_mx a
`polyfun F`	F is continuous with \|F x\| <= C (1 + \|x\|^k)
`mx_polyfun A`	every entry of the matrix function A is a polyfun
`mxpow_deriv W E k`	\sum_(r < k) W ^+ r m E m W ^+ (k.-1 - r)

Main results

Results	Statement
goe_mxgoe_schwinger_dysongoe_tr_sdgauss_ibp_polyfun	The GOE matrix `goe_mx a = (A + A^T) / sqrt (2 d)`, `A = vec_mx a`, for `a` of law `gauss (d * d)`, and the Schwinger-Dyson equation `E tr W^(k+1) = (k E tr W^(k-1) + \sum_(r < k) E[tr W^r tr W^(k-1-r)]) / d`, by Gaussian integration by parts in each coordinate of `a` (for continuous functions of polynomial growth, `polyfun`) and the derivative of matrix powers (`is_derive_mxpow`).
goe_opnorm_meangoe_opnorm_mgfgoe_opnorm_tail_small	`E opnorm W <= 2 sqrt 2` for `d >= 1` (from Gordon's bound `gauss_opnorm_mean`), `E exp (s opnorm W) <= exp (2 sqrt 2 s + s^2 / d)` for `s >= 0`, and `P(opnorm W >= c)` tends to 0 for every `c > 2 sqrt 2`.
goe_tr_vargoe_tr_var_smallRintegral_var_leRintegral_cov_le	`Var (tr W^k / d)` tends to 0, with the bound `2 L^2 + 8 (2k)! exp (2 sqrt 2 (2u + 1) + (2u + 1)^2 / d - 6u)` for every `u >= 0`, `L = sqrt 2 k 3^(k-1) / d`: the statistic of the eigenvalues clipped to `[-3, 3]` is `L`-Lipschitz (Hoffman-Wielandt) and obeys the Gaussian Poincare inequality. `\|Cov (X, Y)\| <= (Var X + Var Y) / 2`.

Declarations77 exported

sectionpolyfun

Context {R : realType}.

lemma continuous_mxentry source, line 93

forall {R : realType} [m n : nat] [i : 'I_m] [j : 'I_n],
continuous (fun M : 'M_(m, n) => M i j)

Statement as written in the source

Lemma continuous_mxentry m n (i : 'I_m) (j : 'I_n) :
  continuous (fun M : 'M[R]_(m, n) => M i j).

Used by 1 declaration in 1 file

this file: polyfun_coord

lemma exprn_le1D source, line 103

forall {R : realType} [t : R] (a b : nat), 0 <= t -> t ^+ a <= 1 + t ^+ (a + b)

Statement as written in the source

Lemma exprn_le1D (t : R) a b : 0 <= t -> t ^+ a <= 1 + t ^+ (a + b).

Used by 2 declarations in 1 file

this file: poly_bound_le, polyfunM

lemma poly_bound_le source, line 111

forall {R : realType} [t C : R] (a b : nat),
0 <= t -> 0 <= C -> C * (1 + t ^+ a) <= 2 * C * (1 + t ^+ (a + b))

Statement as written in the source

Lemma poly_bound_le (t C : R) a b : 0 <= t -> 0 <= C ->
  C * (1 + t ^+ a) <= (2 * C) * (1 + t ^+ (a + b)).

Used by 1 declaration in 1 file

this file: polyfun_bound2

Context {m : nat}.
Implicit Types F G : 'rV[R]_m -> R.

definition polyfun source, line 123

Type

forall {R : realType} {m : nat}, ('rV_m -> R) -> Prop

Definition

Definition polyfun F :=
  continuous F /\ exists (C : R) (k : nat), forall x, `|F x| <= C * (1 + `|x| ^+ k).

Continuous functions of polynomial growth on 'rV[R]_m, the integrands of Gaussian integration by parts (gauss_ibp).

Used by 26 declarations in 3 files

this file: polyfun_bound2, polyfun_cst, polyfun_coord, polyfunD, polyfunM, polyfunB, polyfun_sum, mx_polyfun, polyfun_trace, integrable_polyfun, Rintegral_polyfunD, Rintegral_polyfunZ, Rintegral_polyfun_sum, gauss_ibp_polyfun, Rintegral_var_le, Rintegral_sqr_le, Rintegral_cov_le, gauss_frobenius_mean, polyfun_goe_tr, polyfun_goe_clip, goe_clip_err2, goe_tr_var, goe_schwinger_dyson
GaussianAnalysis.random_matrix.wigner: polyfun_goe_stat_clip, goe_stat_clip_mean_cvg
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_ibp_coord

lemma polyfun_bound2 source, line 127

forall {R : realType} {m : nat} [F G : 'rV_m -> R],
polyfun F ->
polyfun G ->
exists (C : R) (k : nat),
  (forall x : 'rV_m, `|F x| <= C * (1 + `|x| ^+ k)) /\
  (forall x : 'rV_m, `|G x| <= C * (1 + `|x| ^+ k))

Two functions of polynomial growth have a common bound.

Statement as written in the source

Lemma polyfun_bound2 F G : polyfun F -> polyfun G ->
  exists (C : R) (k : nat), (forall x, `|F x| <= C * (1 + `|x| ^+ k)) /\
              (forall x, `|G x| <= C * (1 + `|x| ^+ k)).

Used by 2 declarations in 1 file

this file: polyfunD, gauss_ibp_polyfun

lemma polyfun_cst source, line 142

forall {R : realType} {m : nat} (c : R), polyfun (fun=> c)

Statement as written in the source

Lemma polyfun_cst c : polyfun (fun=> c).

Used by 17 declarations in 3 files

this file: polyfunB, polyfun_sum, mx_polyfun_cst, mx_polyfunZ, Rintegral_var_le, Rintegral_sqr_le, Rintegral_cov_le, mx_polyfun_goe, gauss_frobenius_mean, polyfun_goe_tr, goe_tr_var, goe_schwinger_dyson
GaussianAnalysis.random_matrix.wigner: goe_clip_cvg, goe_stat_clip_mean_cvg
GaussianAnalysis.random_matrix.matrix_series: mx_polyfun_series, gauss_mx_series_ibp_coord, gauss_mx_series_trace_rec

lemma polyfun_coord source, line 148

forall {R : realType} {m : nat} (p : 'I_m), polyfun (fun x : 'rV_m => x 0 p)

Statement as written in the source

Lemma polyfun_coord (p : 'I_m) : polyfun (fun x => x 0 p).

Used by 6 declarations in 2 files

this file: mx_polyfun_goe, gauss_frobenius_mean, goe_schwinger_dyson
GaussianAnalysis.random_matrix.matrix_series: mx_polyfun_series, gauss_mx_series_ibp_coord, gauss_mx_series_ibp

lemma polyfunD source, line 155

forall {R : realType} {m : nat} [F G : 'rV_m -> R],
polyfun F -> polyfun G -> polyfun (fun x : 'rV_m => F x + G x)

Statement as written in the source

Lemma polyfunD F G : polyfun F -> polyfun G -> polyfun (fun x => F x + G x).

Used by 9 declarations in 1 file

this file: polyfunB, polyfun_sum, mx_polyfunD, Rintegral_var_le, Rintegral_sqr_le, Rintegral_cov_le, mx_polyfun_goe, gauss_frobenius_mean, goe_tr_var

lemma polyfunM source, line 163

forall {R : realType} {m : nat} [F G : 'rV_m -> R],
polyfun F -> polyfun G -> polyfun (fun x : 'rV_m => F x * G x)

Statement as written in the source

Lemma polyfunM F G : polyfun F -> polyfun G -> polyfun (fun x => F x * G x).

Used by 19 declarations in 3 files

this file: polyfunB, mx_polyfunZ, mx_polyfun_mul, Rintegral_var_le, Rintegral_sqr_le, Rintegral_cov_le, mx_polyfun_goe, gauss_frobenius_mean, polyfun_goe_tr, goe_clip_err2, goe_tr_var, goe_schwinger_dyson, goe_tr_sd
GaussianAnalysis.random_matrix.wigner: goe_clip_cvg, goe_stat_clip_mean_cvg
GaussianAnalysis.random_matrix.matrix_series: mx_polyfun_series, gauss_mx_series_ibp_coord, gauss_mx_series_ibp, gauss_mx_series_trace_rec

lemma polyfunB source, line 179

forall {R : realType} {m : nat} [F G : 'rV_m -> R],
polyfun F -> polyfun G -> polyfun (fun x : 'rV_m => F x - G x)

Statement as written in the source

Lemma polyfunB F G : polyfun F -> polyfun G -> polyfun (fun x => F x - G x).

Used by 6 declarations in 2 files

this file: Rintegral_sqr_le, Rintegral_cov_le, goe_clip_err2, goe_tr_var
GaussianAnalysis.random_matrix.wigner: goe_clip_cvg, goe_stat_clip_mean_cvg

lemma polyfun_sum source, line 185

forall {R : realType} {m : nat} [I : Type] (s : seq I) [F : I -> 'rV_m -> R],
(forall i : I, polyfun (F i)) -> polyfun (fun x : 'rV_m => \sum_(i <- s) F i x)

Statement as written in the source

Lemma polyfun_sum (I : Type) (s : seq I) (F : I -> 'rV[R]_m -> R) :
  (forall i, polyfun (F i)) -> polyfun (fun x => \sum_(i <- s) F i x).

Used by 9 declarations in 3 files

this file: mx_polyfun_mul, mx_polyfun_sum, polyfun_trace, gauss_frobenius_mean, goe_schwinger_dyson
GaussianAnalysis.random_matrix.wigner: goe_stat_clip_mean_cvg
GaussianAnalysis.random_matrix.matrix_series: mx_polyfun_series, gauss_mx_series_ibp_coord, gauss_mx_series_trace_rec

definition mx_polyfun source, line 194

Type

forall {R : realType} {m : nat} [p q : nat], ('rV_m -> 'M_(p, q)) -> Prop

Definition

Definition mx_polyfun p q (A : 'rV[R]_m -> 'M[R]_(p, q)) :=
  forall i j, polyfun (fun x => A x i j).

Matrices whose entries are continuous functions of polynomial growth.

Used by 10 declarations in 2 files

this file: mx_polyfun_cst, mx_polyfunD, mx_polyfunZ, mx_polyfun_mul, mx_polyfun_sum, mx_polyfun_exp, polyfun_trace, mx_polyfun_mxpow_deriv, mx_polyfun_goe
GaussianAnalysis.random_matrix.matrix_series: mx_polyfun_series

lemma mx_polyfun_cst source, line 197

forall {R : realType} {m : nat} [p q : nat] (B : 'M_(p, q)), mx_polyfun (fun=> B)

Statement as written in the source

Lemma mx_polyfun_cst p q (B : 'M[R]_(p, q)) : mx_polyfun (fun=> B).

Used by 4 declarations in 2 files

this file: mx_polyfun_exp, mx_polyfun_mxpow_deriv
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_ibp, gauss_mx_series_trace_rec

lemma mx_polyfunD source, line 200

forall {R : realType} {m : nat} [p q : nat] [A B : 'rV_m -> 'M_(p, q)],
mx_polyfun A -> mx_polyfun B -> mx_polyfun (fun x : 'rV_m => A x + B x)

Statement as written in the source

Lemma mx_polyfunD p q (A B : 'rV[R]_m -> 'M[R]_(p, q)) :
  mx_polyfun A -> mx_polyfun B -> mx_polyfun (fun x => A x + B x).

lemma mx_polyfunZ source, line 206

forall {R : realType} {m : nat} [p q : nat] (c : R) [A : 'rV_m -> 'M_(p, q)],
mx_polyfun A -> mx_polyfun (fun x : 'rV_m => c *: A x)

Statement as written in the source

Lemma mx_polyfunZ p q c (A : 'rV[R]_m -> 'M[R]_(p, q)) :
  mx_polyfun A -> mx_polyfun (fun x => c *: A x).

lemma mx_polyfun_mul source, line 213

forall {R : realType} {m : nat} [p q r : nat] [A : 'rV_m -> 'M_(p, q)]
  [B : 'rV_m -> 'M_(q, r)],
mx_polyfun A -> mx_polyfun B -> mx_polyfun (fun x : 'rV_m => A x *m B x)

Statement as written in the source

Lemma mx_polyfun_mul p q r (A : 'rV[R]_m -> 'M[R]_(p, q))
    (B : 'rV[R]_m -> 'M[R]_(q, r)) :
  mx_polyfun A -> mx_polyfun B -> mx_polyfun (fun x => A x *m B x).

Used by 4 declarations in 2 files

this file: mx_polyfun_exp, mx_polyfun_mxpow_deriv
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_ibp, gauss_mx_series_trace_rec

lemma mx_polyfun_sum source, line 221

forall {R : realType} {m : nat} [I : Type] (s : seq I) [p q : nat]
  [A : I -> 'rV_m -> 'M_(p, q)],
(forall i : I, mx_polyfun (A i)) -> mx_polyfun (fun x : 'rV_m => \sum_(i <- s) A i x)

Statement as written in the source

Lemma mx_polyfun_sum (I : Type) (s : seq I) p q
    (A : I -> 'rV[R]_m -> 'M[R]_(p, q)) :
  (forall i, mx_polyfun (A i)) -> mx_polyfun (fun x => \sum_(i <- s) A i x).

Used by 1 declaration in 1 file

this file: mx_polyfun_mxpow_deriv

lemma mx_polyfun_exp source, line 229

forall {R : realType} {m : nat} [p : nat] [A : 'rV_m -> 'M_p] (k : nat),
mx_polyfun A -> mx_polyfun (fun x : 'rV_m => A x ^+ k)

Statement as written in the source

Lemma mx_polyfun_exp p (A : 'rV[R]_m -> 'M[R]_p) k :
  mx_polyfun A -> mx_polyfun (fun x => A x ^+ k).

Used by 10 declarations in 3 files

this file: mx_polyfun_mxpow_deriv, polyfun_goe_tr, goe_schwinger_dyson, goe_tr_sd
GaussianAnalysis.random_matrix.wigner: goe_moment_cvg
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_ibp_coord, gauss_mx_series_ibp, gauss_mx_series_trace_rec, gauss_mx_series_moment, gauss_mx_series_opnorm_moment

lemma polyfun_trace source, line 237

forall {R : realType} {m : nat} [p : nat] [A : 'rV_m -> 'M_p],
mx_polyfun A -> polyfun (fun x : 'rV_m => \tr (A x))

Statement as written in the source

Lemma polyfun_trace p (A : 'rV[R]_m -> 'M[R]_p) :
  mx_polyfun A -> polyfun (fun x => \tr (A x)).

Used by 8 declarations in 3 files

this file: polyfun_goe_tr, goe_schwinger_dyson, goe_tr_sd
GaussianAnalysis.random_matrix.wigner: goe_moment_cvg
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_ibp, gauss_mx_series_trace_rec, gauss_mx_series_moment, gauss_mx_series_opnorm_moment

sectionmxpow_derive

Context {R : realType} {n : nat}.
Implicit Types W E : 'M[R]_n.

definition mxpow_deriv source, line 248

Type

forall {R : realType} {n : nat}, 'M_n -> 'M_n -> nat -> 'M_n

Definition

Definition mxpow_deriv W E k : 'M[R]_n :=
  \sum_(r < k) W ^+ r *m E *m W ^+ (k.-1 - r).

The derivative of M |-> M ^+ k at W along E.

Used by 13 declarations in 2 files

this file: mxpow_derivS, is_derive_mxpow, mxpow_derivD, mxpow_derivZ, mxpow_deriv_trace, mx_polyfun_mxpow_deriv, is_derive_goe_pow, goe_schwinger_dyson
GaussianAnalysis.random_matrix.matrix_series: is_derive_series_pow, gauss_mx_series_ibp_coord, gauss_mx_series_ibp, gauss_mx_series_trace_sqr, gauss_mx_series_trace_rec

lemma mxpow_derivS source, line 251

forall {R : realType} {n : nat} (W E : 'M_n) (k : nat),
mxpow_deriv W E k.+1 = mxpow_deriv W E k *m W + W ^+ k *m E

Statement as written in the source

Lemma mxpow_derivS W E k :
  mxpow_deriv W E k.+1 = mxpow_deriv W E k *m W + W ^+ k *m E.

Used by 1 declaration in 1 file

this file: is_derive_mxpow

lemma is_derive_mxentry source, line 262

forall {R : realType} {n : nat} (W E : 'M_n) (i j : 'I_n),
is_derive W E (fun M : 'M_n => M i j) (E i j)

Statement as written in the source

Lemma is_derive_mxentry W E (i j : 'I_n) :
  is_derive W E (fun M : 'M[R]_n => M i j) (E i j).

Used by 1 declaration in 1 file

this file: is_derive_mxpow

lemma is_derive_mxpow source, line 273

forall {R : realType} {n : nat} (W E : 'M_n) (k : nat) (i j : 'I_n),
is_derive W E (fun M : 'M_n => (M ^+ k) i j) (mxpow_deriv W E k i j)

Statement as written in the source

Lemma is_derive_mxpow W E k (i j : 'I_n) :
  is_derive W E (fun M : 'M[R]_n => (M ^+ k) i j) (mxpow_deriv W E k i j).

Used by 2 declarations in 2 files

this file: is_derive_goe_pow
GaussianAnalysis.random_matrix.matrix_series: is_derive_series_pow

lemma mxpow_derivD source, line 292

forall {R : realType} {n : nat} (W E : 'M_n)
  (F : 'M[R]_(n, n)) (k : nat),
mxpow_deriv W (E + F) k = mxpow_deriv W E k + mxpow_deriv W F k

Statement as written in the source

Lemma mxpow_derivD W E F k :
  mxpow_deriv W (E + F) k = mxpow_deriv W E k + mxpow_deriv W F k.

lemma mxpow_derivZ source, line 299

forall {R : realType} {n : nat} (W E : 'M_n) (c : R) (k : nat),
mxpow_deriv W (c *: E) k = c *: mxpow_deriv W E k

Statement as written in the source

Lemma mxpow_derivZ W E c k : mxpow_deriv W (c *: E) k = c *: mxpow_deriv W E k.

Used by 1 declaration in 1 file

this file: goe_schwinger_dyson

lemma mulmx_delta_entry source, line 305

forall {R : realType} {n : nat} [p q : nat] (A : 'M_(p, n)) (B : 'M_(n, q))
  (i j : 'I_n) (a : 'I_p) 
  (b : 'I_q),
(A *m delta_mx i j *m B) a b = A a i * B j b

Statement as written in the source

Lemma mulmx_delta_entry p q (A : 'M[R]_(p, n)) (B : 'M[R]_(n, q)) i j a b :
  (A *m delta_mx i j *m B) a b = A a i * B j b.

Used by 1 declaration in 1 file

this file: mxpow_deriv_trace

lemma trmx_exp source, line 316

forall {R : realType} {n : nat} (W : 'M_n) (k : nat), (W ^+ k)^T = W^T ^+ k

Statement as written in the source

Lemma trmx_exp W k : (W ^+ k)^T = W^T ^+ k.

Used by 2 declarations in 1 file

this file: mxpow_deriv_trace, goe_schwinger_dyson

lemma mxpow_deriv_trace source, line 325

forall {R : realType} {n : nat} [W : 'M_n] (k : nat),
W^T = W ->
\sum_i \sum_j mxpow_deriv W (delta_mx i j + delta_mx j i) k j i =
k%:R * \tr (W ^+ k.-1) + \sum_(r < k) \tr (W ^+ r) * \tr (W ^+ (k.-1 - r))

The sum over (i, j) of the entries (j, i) of the derivative of W^k along E_ij + E_ji: k tr W^(k-1) + \sum_(r < k) tr W^r tr W^(k-1-r) for W symmetric.

Statement as written in the source

Lemma mxpow_deriv_trace W k : W^T = W ->
  \sum_i \sum_j mxpow_deriv W (delta_mx i j + delta_mx j i) k j i =
  k%:R * \tr (W ^+ k.-1) + \sum_(r < k) \tr (W ^+ r) * \tr (W ^+ (k.-1 - r)).

Used by 1 declaration in 1 file

this file: goe_schwinger_dyson

sectionmxpow_polyfun

Context {R : realType} {m n : nat}.

lemma mx_polyfun_mxpow_deriv source, line 356

forall {R : realType} {m n : nat} [A : 'rV_m -> 'M_n] (E : 'M_n) (k : nat),
mx_polyfun A -> mx_polyfun (fun x : 'rV_m => mxpow_deriv (A x) E k)

Statement as written in the source

Lemma mx_polyfun_mxpow_deriv (A : 'rV[R]_m -> 'M[R]_n) (E : 'M[R]_n) k :
  mx_polyfun A -> mx_polyfun (fun x => mxpow_deriv (A x) E k).

Used by 3 declarations in 2 files

this file: goe_schwinger_dyson
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_ibp_coord, gauss_mx_series_trace_rec

lemma integrable_polyfun source, line 365

forall {R : realType} {m : nat} [F : 'rV_m -> R],
polyfun F -> (gauss m).-integrable [set: 'rV_m] (EFin \o F)

Integrals of functions of polynomial growth against gauss m.

Statement as written in the source

Lemma integrable_polyfun (F : 'rV[R]_m -> R) : polyfun F ->
  (gauss m).-integrable [set: 'rV[R]_m] (EFin \o F).

Used by 10 declarations in 3 files

this file: Rintegral_polyfunD, Rintegral_polyfunZ, Rintegral_polyfun_sum, Rintegral_cov_le, gauss_frobenius_mean, goe_clip_err2, goe_tr_var
GaussianAnalysis.random_matrix.wigner: goe_stat_clip_mean_cvg
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_trace_rec, gauss_mx_series_moment

lemma Rintegral_polyfunD source, line 372

forall {R : realType} {m : nat} [F G : 'rV_m -> R],
polyfun F ->
polyfun G -> \int[gauss m]_x (F x + G x) = \int[gauss m]_x F x + \int[gauss m]_x G x

Statement as written in the source

Lemma Rintegral_polyfunD (F G : 'rV[R]_m -> R) : polyfun F -> polyfun G ->
  \int[gauss m]_x (F x + G x) = \int[gauss m]_x F x + \int[gauss m]_x G x.

Used by 7 declarations in 2 files

this file: Rintegral_var_le, Rintegral_sqr_le, Rintegral_cov_le, gauss_frobenius_mean, goe_tr_var, goe_schwinger_dyson
GaussianAnalysis.random_matrix.wigner: goe_clip_cvg

lemma Rintegral_polyfunZ source, line 376

forall {R : realType} {m : nat} (c : R) [F : 'rV_m -> R],
polyfun F -> \int[gauss m]_x (c * F x) = c * \int[gauss m]_x F x

Statement as written in the source

Lemma Rintegral_polyfunZ c (F : 'rV[R]_m -> R) : polyfun F ->
  \int[gauss m]_x (c * F x) = c * \int[gauss m]_x F x.

Used by 12 declarations in 3 files

this file: Rintegral_var_le, Rintegral_sqr_le, Rintegral_cov_le, gauss_frobenius_mean, goe_tr_var, goe_schwinger_dyson, goe_tr_sd
GaussianAnalysis.random_matrix.wigner: goe_moment_cvg, goe_clip_cvg, goe_stat_clip_mean_cvg
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_ibp_coord, gauss_mx_series_trace_rec

lemma Rintegral_polyfun_sum source, line 380

forall {R : realType} {m : nat} [I : Type] (s : seq I) [F : I -> 'rV_m -> R],
(forall i : I, polyfun (F i)) ->
\int[gauss m]_x \sum_(i <- s) F i x = \sum_(i <- s) \int[gauss m]_x F i x

Statement as written in the source

Lemma Rintegral_polyfun_sum (I : Type) (s : seq I) (F : I -> 'rV[R]_m -> R) :
  (forall i, polyfun (F i)) ->
  \int[gauss m]_x (\sum_(i <- s) F i x) = \sum_(i <- s) \int[gauss m]_x F i x.

Used by 5 declarations in 3 files

this file: goe_schwinger_dyson
GaussianAnalysis.random_matrix.wigner: goe_stat_clip_mean_cvg
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_ibp_coord, gauss_mx_series_ibp, gauss_mx_series_trace_rec

lemma gauss_ibp_polyfun main result source, line 386

forall {R : realType} {m : nat} [p : 'I_m] [F dF : 'rV_m -> R],
(forall x : 'rV[R]_m,
 is_derive x 'e_p F (dF x)) ->
polyfun F -> polyfun dF -> \int[gauss m]_x (x 0 p * F x) = \int[gauss m]_x dF x

Gaussian integration by parts for functions of polynomial growth.

Main result

Stated in the README together with goe_mx.

Statement as written in the source

Lemma gauss_ibp_polyfun (p : 'I_m) (F dF : 'rV[R]_m -> R) :
  (forall x, is_derive x (delta_mx 0 p) F (dF x)) -> polyfun F -> polyfun dF ->
  \int[gauss m]_x (x 0 p * F x) = \int[gauss m]_x dF x.

Used by 2 declarations in 2 files

this file: goe_schwinger_dyson
GaussianAnalysis.random_matrix.matrix_series: gauss_mx_series_ibp_coord

lemma Rintegral_var_le main result source, line 395

forall {R : realType} {m : nat} [X : 'rV_m -> R] (c : R),
polyfun X ->
\int[gauss m]_x (X x - \int[gauss m]_y X y) ^+ 2 <= \int[gauss m]_x (X x - c) ^+ 2

The variance is the least mean square deviation.

Main result

Stated in the README together with goe_tr_var.

Statement as written in the source

Lemma Rintegral_var_le (X : 'rV[R]_m -> R) (c : R) : polyfun X ->
  \int[gauss m]_x (X x - \int[gauss m]_y X y) ^+ 2 <=
  \int[gauss m]_x (X x - c) ^+ 2.

Used by 1 declaration in 1 file

this file: goe_tr_var

lemma Rintegral_sqr_le source, line 424

forall {R : realType} {m : nat} [X : 'rV_m -> R],
polyfun X -> (\int[gauss m]_x X x) ^+ 2 <= \int[gauss m]_x X x ^+ 2

(E X)^2 <= E X^2.

Statement as written in the source

Lemma Rintegral_sqr_le (X : 'rV[R]_m -> R) : polyfun X ->
  (\int[gauss m]_x X x) ^+ 2 <= \int[gauss m]_x X x ^+ 2.

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.wigner: goe_clip_cvg

lemma Rintegral_cov_le main result source, line 449

forall {R : realType} {m : nat} [X Y : 'rV_m -> R],
polyfun X ->
polyfun Y ->
`|\int[gauss m]_x (X x * Y x) - \int[gauss m]_x X x * \int[gauss m]_x Y x| <=
(\int[gauss m]_x (X x - \int[gauss m]_y X y) ^+ 2 +
 \int[gauss m]_x (Y x - \int[gauss m]_y Y y) ^+ 2) /
2

|Cov (X, Y)| <= (Var X + Var Y) / 2.

Main result

Stated in the README together with goe_tr_var.

Statement as written in the source

Lemma Rintegral_cov_le (X Y : 'rV[R]_m -> R) : polyfun X -> polyfun Y ->
  `|\int[gauss m]_x (X x * Y x) -
    \int[gauss m]_x X x * \int[gauss m]_x Y x| <=
  (\int[gauss m]_x (X x - \int[gauss m]_y X y) ^+ 2 +
   \int[gauss m]_x (Y x - \int[gauss m]_y Y y) ^+ 2) / 2.

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.wigner: goe_tr_cov_cvg

lemma gauss_tail_expR source, line 497

forall {R : realType} {m : nat} [F : 'rV_m -> R] (c : R) [s : R],
measurable_fun [set: 'rV_m] F ->
0 <= s ->
(gauss m).-integrable [set: 'rV_m] (EFin \o (fun x : 'rV_m => expR (s * F x))) ->
(gauss m [set x | (c <= F x)%R] <= (expR (- (s * c)) * \int[gauss m]_x expR (s * F x))%:E)%E

Markov's inequality for the exponential: P(F >= c) <= exp (- s c) E exp (s F) for s >= 0.

Statement as written in the source

Lemma gauss_tail_expR (F : 'rV[R]_m -> R) (c s : R) :
  measurable_fun [set: 'rV[R]_m] F -> 0 <= s ->
  (gauss m).-integrable [set: 'rV[R]_m] (EFin \o (fun x => expR (s * F x))) ->
  (gauss m [set x | (c <= F x)%R] <=
   (expR (- (s * c)) * \int[gauss m]_x expR (s * F x))%R%:E)%E.

Used by 1 declaration in 1 file

this file: goe_opnorm_tail_small

sectiongoe

Context {R : realType}.

definition goe_mx main result source, line 536

Type

forall {R : realType} [d : nat], 'rV_(d * d) -> 'M_d

Definition

Definition goe_mx d (a : 'rV[R]_(d * d)) : 'M[R]_d :=
  (Num.sqrt (2 * d%:R))^-1 *: (vec_mx a + (vec_mx a)^T).

The GOE matrix (A + A^T) / sqrt (2 d) of a row vector of size d * d.

Main result, as the README states it

The GOE matrix goe_mx a = (A + A^T) / sqrt (2 d), A = vec_mx a, for a of law gauss (d * d), and the Schwinger-Dyson equation E tr W^(k+1) = (k E tr W^(k-1) + \sum_(r < k) E[tr W^r tr W^(k-1-r)]) / d, by Gaussian integration by parts in each coordinate of a (for continuous functions of polynomial growth, polyfun) and the derivative of matrix powers (is_derive_mxpow).

Used by 80 declarations in 8 files

this file: goe_mx_sym, goe_mxE, goe_mxD, goe_mxZ, goe_mx_delta, mx_polyfun_goe, is_derive_goe_pow, goe_mxB, frobenius_goe_mx, goe_opnorm_lipschitz, integrable_goe_opnorm, opnorm_goe_mx, goe_opnorm_mean, integrable_goe_opnorm_expR, goe_opnorm_mgf, goe_mx_symmetric, goe_tr, goe_clip, goe_trE, goe_clip_err, goe_clip_err2, goe_tr_var, goe_schwinger_dyson, goe_tr_sd, goe_opnorm_tail_small
GaussianAnalysis.random_matrix.goe_edge: goe_mx_form, goe_mxN, goe_form_mxE, goe_lambda_max_lipschitz, goe_lambda_maxN_lipschitz, measurable_goe_lambda_max, measurable_goe_lambda_maxN, integrable_goe_lambda_max, integrable_goe_lambda_maxN, goe_lambda_max_mean, goe_lambda_maxN_mean, goe_lambda_max_tail, goe_lambda_maxN_tail, goe_opnorm_edge_tail
GaussianAnalysis.random_matrix.goe_rotation: goe_mx_conj, measurable_goe_mx, goe_conj_integral, goe_equiv_form, goe_equiv_formR, goe_equiv_diag, goe_equiv_pair, mX, qintXX, goe_equiv_diag2, goe_equiv_pair2, goe_diag_var_identityS, goe_diag_var_identity, goe_diag_var_tail
GaussianAnalysis.random_matrix.wigner: goe_stat, continuous_goe_stat, wigner, goe_stat_near, wigner_uniform
GaussianAnalysis.random_matrix.goe_entries: goe_mx_mxdot, goe_mx_diag_tail, goe_mx_offdiag_tail, goe_mx_row_tail, measurable_goe_entry, measurable_goe_entry_ge, measurable_goe_row_ge, measurable_goe_opnorm_ge, measurable_goe_diag_max, measurable_goe_offdiag_max, measurable_goe_row_max, goe_mx_diag_max_tail, goe_mx_offdiag_max_tail, goe_mx_row_max_tail
GaussianApplications.GoeEdgeStatement: goe_edge_statement
GaussianApplications.SKGapDefinitions: sk_coupling
GaussianApplications.SKGap.Disorder: sk_couplingE, sk_coupling_opnorm_le, sk_coupling_row, sk_couplingB, frobenius_sk_coupling_le, sk_good_disorder_prob

lemma goe_mx_sym source, line 539

forall {R : realType} [d : nat] (a : 'rV_(d * d)), (goe_mx a)^T = goe_mx a

Statement as written in the source

Lemma goe_mx_sym d (a : 'rV[R]_(d * d)) : (goe_mx a)^T = goe_mx a.

Used by 3 declarations in 2 files

this file: goe_mx_symmetric, goe_schwinger_dyson
GaussianApplications.SKGap.Poincare: sk_coupling_sym

lemma goe_mxE source, line 542

forall {R : realType} [d : nat] (a : 'rV_(d * d)) (i j : 'I_d),
goe_mx a i j =
(Num.ExtraDef.sqrtr (2 * d%:R))^-1 * (a 0 (mxvec_index i j) + a 0 (mxvec_index j i))

Statement as written in the source

Lemma goe_mxE d (a : 'rV[R]_(d * d)) i j :
  goe_mx a i j =
  (Num.sqrt (2 * d%:R))^-1 * (a 0 (mxvec_index i j) + a 0 (mxvec_index j i)).

Used by 5 declarations in 2 files

this file: goe_mxD, goe_mxZ, mx_polyfun_goe, goe_schwinger_dyson
GaussianAnalysis.random_matrix.goe_entries: goe_mx_mxdot

lemma goe_mxD source, line 547

forall {R : realType} [d : nat] (a b : 'rV_(d * d)), goe_mx (a + b) = goe_mx a + goe_mx b

Statement as written in the source

Lemma goe_mxD d (a b : 'rV[R]_(d * d)) : goe_mx (a + b) = goe_mx a + goe_mx b.

Used by 2 declarations in 1 file

this file: is_derive_goe_pow, goe_mxB

lemma goe_mxZ source, line 550

forall {R : realType} [d : nat] (h : R) (a : 'rV_(d * d)), goe_mx (h *: a) = h *: goe_mx a

Statement as written in the source

Lemma goe_mxZ d (h : R) (a : 'rV[R]_(d * d)) : goe_mx (h *: a) = h *: goe_mx a.

Used by 3 declarations in 2 files

this file: is_derive_goe_pow, goe_mxB
GaussianAnalysis.random_matrix.goe_edge: goe_mxN

lemma goe_mx_delta source, line 553

forall {R : realType} [d : nat] (i j : 'I_d),
goe_mx 'e_(mxvec_index i j) =
(Num.ExtraDef.sqrtr (2 * d%:R))^-1 *: (delta_mx i j + delta_mx j i)

Statement as written in the source

Lemma goe_mx_delta d (i j : 'I_d) :
  goe_mx (delta_mx 0 (mxvec_index i j)) =
  (Num.sqrt (2 * d%:R))^-1 *: (delta_mx i j + delta_mx j i).

Used by 1 declaration in 1 file

this file: goe_schwinger_dyson

lemma mx_polyfun_goe source, line 558

forall {R : realType} [d : nat], mx_polyfun (goe_mx (d:=d))

Statement as written in the source

Lemma mx_polyfun_goe d : mx_polyfun (@goe_mx d).

Used by 5 declarations in 3 files

this file: polyfun_goe_tr, goe_schwinger_dyson, goe_tr_sd
GaussianAnalysis.random_matrix.goe_rotation: measurable_goe_mx
GaussianAnalysis.random_matrix.wigner: goe_moment_cvg

lemma is_derive_goe_pow source, line 564

forall {R : realType} [d : nat] (k : nat) (i j : 'I_d) (x v : 'rV_(d * d)),
is_derive x v
  (fun a : 'rV[R]_(d * d) =>
   (goe_mx a ^+ k) i j)
  (mxpow_deriv (goe_mx x) (goe_mx v) k i j)

Statement as written in the source

Lemma is_derive_goe_pow d k (i j : 'I_d) (x v : 'rV[R]_(d * d)) :
  is_derive x v (fun a => (goe_mx a ^+ k) i j)
    (mxpow_deriv (goe_mx x) (goe_mx v) k i j).

Used by 1 declaration in 1 file

this file: goe_schwinger_dyson

sectiongauss_frobenius_mean

Context {R : realType} (n : nat).

lemma gauss_frobenius_mean source, line 579

forall {R : realType} (n : nat), \int[gauss n]_g frobenius g <= Num.ExtraDef.sqrtr n%:R

E |g| <= sqrt n for g of law gauss n, by 2 |g| sqrt n <= |g|^2 + n.

Statement as written in the source

Lemma gauss_frobenius_mean :
  \int[@gauss R n]_g frobenius g <= Num.sqrt n%:R.

Used by 2 declarations in 2 files

this file: goe_opnorm_mean
GaussianAnalysis.random_matrix.goe_edge: goe_form_max_mean

sectiongoe_opnorm

Context {R : realType} (d : nat).
Local Notation gauss := (@gauss R).

lemma goe_mxB source, line 626

forall {R : realType} [d : nat] (a b : 'rV_(d * d)), goe_mx (a - b) = goe_mx a - goe_mx b

Statement as written in the source

Lemma goe_mxB (a b : 'rV[R]_(d * d)) : goe_mx (a - b) = goe_mx a - goe_mx b.

Used by 7 declarations in 5 files

this file: goe_opnorm_lipschitz, goe_clip_lipschitz
GaussianAnalysis.random_matrix.goe_edge: goe_lambda_max_lipschitz
GaussianAnalysis.random_matrix.wigner: goe_stat_lipschitz, continuous_goe_stat
GaussianAnalysis.random_matrix.goe_entries: measurable_goe_opnorm_ge
GaussianApplications.SKGap.Disorder: sk_couplingB

lemma two_div_sqrt source, line 629

forall {R : realType} (d : nat),
2 / Num.ExtraDef.sqrtr (2 * d%:R) = Num.ExtraDef.sqrtr (2 / d%:R)

Statement as written in the source

Lemma two_div_sqrt : 2 * (Num.sqrt (2 * d%:R))^-1 = Num.sqrt (2 / d%:R) :> R.

Used by 3 declarations in 2 files

this file: frobenius_goe_mx, opnorm_goe_mx
GaussianAnalysis.random_matrix.goe_edge: goe_mx_form

lemma frobenius_goe_mx source, line 640

forall {R : realType} [d : nat] (a : 'rV_(d * d)),
frobenius (goe_mx a) <= Num.ExtraDef.sqrtr (2 / d%:R) * frobenius a

Statement as written in the source

Lemma frobenius_goe_mx (a : 'rV[R]_(d * d)) :
  frobenius (goe_mx a) <= Num.sqrt (2 / d%:R) * frobenius a.

Used by 7 declarations in 5 files

this file: goe_opnorm_lipschitz, goe_clip_lipschitz
GaussianAnalysis.random_matrix.goe_edge: goe_lambda_max_lipschitz
GaussianAnalysis.random_matrix.wigner: goe_stat_lipschitz, continuous_goe_stat
GaussianAnalysis.random_matrix.goe_entries: measurable_goe_opnorm_ge
GaussianApplications.SKGap.Disorder: measurable_sk_coupling_opnorm

lemma goe_opnorm_lipschitz source, line 650

forall {R : realType} [d : nat] (a b : 'rV_(d * d)),
`|opnorm (goe_mx a) - opnorm (goe_mx b)| <=
Num.ExtraDef.sqrtr (2 / d%:R) * frobenius (a - b)

Statement as written in the source

Lemma goe_opnorm_lipschitz (a b : 'rV[R]_(d * d)) :
  `|opnorm (goe_mx a) - opnorm (goe_mx b)| <=
  Num.sqrt (2 / d%:R) * frobenius (a - b).

Used by 6 declarations in 2 files

this file: integrable_goe_opnorm, integrable_goe_opnorm_expR, goe_opnorm_mgf, goe_opnorm_tail_small
GaussianAnalysis.random_matrix.wigner: wigner, wigner_uniform

lemma integrable_goe_opnorm source, line 658

forall {R : realType} (d : nat),
(gauss (d * d)).-integrable [set: 'rV_(d * d)]
  (EFin \o (fun a : 'rV_(d * d) => opnorm (goe_mx a)))

Statement as written in the source

Lemma integrable_goe_opnorm :
  (gauss (d * d)).-integrable [set: 'rV[R]_(d * d)]
    (EFin \o (fun a => opnorm (goe_mx a))).

Used by 2 declarations in 2 files

this file: goe_opnorm_mean
GaussianAnalysis.random_matrix.goe_edge: goe_lambda_max_mean

lemma opnorm_goe_mx source, line 663

forall {R : realType} [d : nat] (a : 'rV_(d * d)),
opnorm (goe_mx a) <= Num.ExtraDef.sqrtr (2 / d%:R) * opnorm (vec_mx a : 'M_d)

Statement as written in the source

Lemma opnorm_goe_mx (a : 'rV[R]_(d * d)) :
  opnorm (goe_mx a) <= Num.sqrt (2 / d%:R) * opnorm (vec_mx a : 'M[R]_(d, d)).

Used by 1 declaration in 1 file

this file: goe_opnorm_mean

lemma goe_opnorm_mean main result source, line 675

forall {R : realType} [d : nat],
(0 < d)%N -> \int[gauss (d * d)]_a opnorm (goe_mx a) <= 2 * Num.ExtraDef.sqrtr 2

E opnorm W <= 2 sqrt 2: opnorm W <= sqrt (2 / d) opnorm A, and E opnorm A <= E |g| + E |h| <= 2 sqrt d by Gordon's inequality (gauss_opnorm_mean).

Main result, as the README states it

E opnorm W <= 2 sqrt 2 for d >= 1 (from Gordon's bound gauss_opnorm_mean), E exp (s opnorm W) <= exp (2 sqrt 2 s + s^2 / d) for s >= 0, and P(opnorm W >= c) tends to 0 for every c > 2 sqrt 2.

Statement as written in the source

Lemma goe_opnorm_mean : (0 < d)%N ->
  \int[gauss (d * d)]_a opnorm (goe_mx a) <= 2 * Num.sqrt 2.

Used by 2 declarations in 2 files

this file: goe_opnorm_mgf
GaussianAnalysis.random_matrix.goe_edge: goe_lambda_max_mean

lemma integrable_goe_opnorm_expR source, line 698

forall {R : realType} (d : nat) (s : R),
(gauss (d * d)).-integrable [set: 'rV_(d * d)]
  (EFin \o (fun a : 'rV_(d * d) => expR (s * opnorm (goe_mx a))))

Statement as written in the source

Lemma integrable_goe_opnorm_expR (s : R) :
  (gauss (d * d)).-integrable [set: 'rV[R]_(d * d)]
    (EFin \o (fun a => expR (s * opnorm (goe_mx a)))).

Used by 3 declarations in 1 file

this file: goe_clip_err2, goe_tr_var, goe_opnorm_tail_small

lemma goe_opnorm_mgf main result source, line 713

forall {R : realType} [d : nat] [s : R],
(0 < d)%N ->
0 <= s ->
\int[gauss (d * d)]_a expR (s * opnorm (goe_mx a)) <=
expR (2 * Num.ExtraDef.sqrtr 2 * s + s ^+ 2 / d%:R)

E exp (s opnorm W) <= exp (2 sqrt 2 s + s^2 / d) for s >= 0: Gaussian concentration of the sqrt (2 / d)-Lipschitz function opnorm W around its mean, which is at most 2 sqrt 2.

Main result

Stated in the README together with goe_opnorm_mean.

Statement as written in the source

Lemma goe_opnorm_mgf (s : R) : (0 < d)%N -> 0 <= s ->
  \int[gauss (d * d)]_a expR (s * opnorm (goe_mx a)) <=
  expR (2 * Num.sqrt 2 * s + s ^+ 2 / d%:R).

Used by 3 declarations in 1 file

this file: goe_clip_err2, goe_tr_var, goe_opnorm_tail_small

sectionclip_pow

Context {R : realType}.

lemma exprB_le source, line 743

forall {R : realType} [M x y : R] (k : nat),
`|x| <= M -> `|y| <= M -> `|x ^+ k - y ^+ k| <= k%:R * M ^+ k.-1 * `|x - y|

|x^k - y^k| <= k M^(k-1) |x - y| for |x|, |y| <= M.

Statement as written in the source

Lemma exprB_le (M x y : R) k : `|x| <= M -> `|y| <= M ->
  `|x ^+ k - y ^+ k| <= k%:R * M ^+ k.-1 * `|x - y|.

Used by 1 declaration in 1 file

this file: clip_pow_lipschitz

lemma clip_pow_lipschitz source, line 757

forall {R : realType} [c : R] (x y : R) (k : nat),
0 <= c -> `|clip c x ^+ k - clip c y ^+ k| <= k%:R * c ^+ k.-1 * `|x - y|

Statement as written in the source

Lemma clip_pow_lipschitz (c x y : R) k : 0 <= c ->
  `|clip c x ^+ k - clip c y ^+ k| <= k%:R * c ^+ k.-1 * `|x - y|.

Used by 1 declaration in 1 file

this file: goe_clip_lipschitz

lemma clip_pow_err source, line 766

forall {R : realType} [c w x u : R] (k : nat),
0 <= c ->
`|x| <= w -> 0 <= u -> `|x ^+ k - clip c x ^+ k| <= 2 * w ^+ k * expR (u * (w - c))

The error of clipping at c a point x with |x| <= w, weighted so as to vanish when w <= c.

Statement as written in the source

Lemma clip_pow_err (c w x u : R) k : 0 <= c -> `|x| <= w -> 0 <= u ->
  `|x ^+ k - clip c x ^+ k| <= 2 * w ^+ k * expR (u * (w - c)).

Used by 1 declaration in 1 file

this file: goe_clip_err

lemma exprn_le_fact_expR source, line 783

forall {R : realType} [x : R] (j : nat), 0 <= x -> x ^+ j <= j`!%:R * expR x

Statement as written in the source

Lemma exprn_le_fact_expR (x : R) j : 0 <= x -> x ^+ j <= j`!%:R * expR x.

Used by 2 declarations in 1 file

this file: goe_clip_err2, goe_tr_var

sectionspec_opnorm

Context {R : realType} {n : nat}.

lemma spec_le_opnorm source, line 797

forall {R : realType} {n : nat} [A : 'M_n] (i : 'I_n),
A \is symmetricmx -> `|spec A 0 i| <= opnorm A

Statement as written in the source

Lemma spec_le_opnorm (A : 'M[R]_n) i : A \is symmetricmx ->
  `|spec A 0 i| <= opnorm A.

Used by 3 declarations in 2 files

this file: goe_clip_err
GaussianAnalysis.random_matrix.wigner: wigner, goe_stat_near

sectiongoe_stats

Context {R : realType} (d : nat).
Local Notation gauss := (@gauss R).

lemma goe_mx_symmetric source, line 810

forall {R : realType} [d : nat] (a : 'rV_(d * d)), goe_mx a \is symmetricmx

Statement as written in the source

Lemma goe_mx_symmetric (a : 'rV[R]_(d * d)) : goe_mx a \is symmetricmx.

Used by 10 declarations in 4 files

this file: goe_trE, goe_clip_err, goe_clip_lipschitz
GaussianAnalysis.random_matrix.goe_edge: goe_opnorm_edge_tail
GaussianAnalysis.random_matrix.goe_rotation: goe_equiv_form, goe_equiv_pair
GaussianAnalysis.random_matrix.wigner: goe_stat_lipschitz, continuous_goe_stat, wigner, goe_stat_near

definition goe_tr source, line 815

Type

forall {R : realType} [d : nat], nat -> 'rV_(d * d) -> R

Definition

Definition goe_tr k (a : 'rV[R]_(d * d)) : R := \tr (goe_mx a ^+ k) / d%:R.

t_k = tr W^k / d and its version with the eigenvalues clipped to [-3, 3].

Used by 11 declarations in 2 files

this file: goe_trE, goe_clip_err, polyfun_goe_tr, goe_clip_err2, goe_tr_var, goe_tr_sd, goe_tr_var_small, goe_clip_err2_small
GaussianAnalysis.random_matrix.wigner: goe_tr_cov_cvg, goe_moment_cvg, goe_clip_cvg

definition goe_clip source, line 817

Type

forall {R : realType} [d : nat], nat -> 'rV_(d * d) -> R

Definition

Definition goe_clip k (a : 'rV[R]_(d * d)) : R :=
  (\sum_i clip 3 (spec (goe_mx a) 0 i) ^+ k) / d%:R.

Used by 10 declarations in 2 files

this file: goe_clip_err, goe_clip_lipschitz, goe_clip_bound, polyfun_goe_clip, goe_clip_err2, goe_tr_var, goe_clip_err2_small
GaussianAnalysis.random_matrix.wigner: goe_clip_cvg, goe_stat_poly_clip, goe_stat_clip_mean_cvg

lemma goe_trE source, line 820

forall {R : realType} [d : nat] (k : nat) (a : 'rV_(d * d)),
goe_tr k a = (\sum_i spec (goe_mx a) 0 i ^+ k) / d%:R

Statement as written in the source

Lemma goe_trE k a :
  goe_tr k a = (\sum_i spec (goe_mx a) 0 i ^+ k) / d%:R.

Used by 1 declaration in 1 file

this file: goe_clip_err

lemma goe_clip_err source, line 824

forall {R : realType} [d : nat] (k : nat) (a : 'rV_(d * d)) [u : R],
0 <= u ->
`|goe_tr k a - goe_clip k a| <=
2 * opnorm (goe_mx a) ^+ k * expR (u * (opnorm (goe_mx a) - 3))

Statement as written in the source

Lemma goe_clip_err k a (u : R) : 0 <= u ->
  `|goe_tr k a - goe_clip k a| <=
  2 * opnorm (goe_mx a) ^+ k * expR (u * (opnorm (goe_mx a) - 3)).

Used by 2 declarations in 1 file

this file: goe_clip_err2, goe_tr_var

lemma goe_clip_lipschitz source, line 842

forall {R : realType} [d : nat] (k : nat) (a b : 'rV_(d * d)),
`|goe_clip k a - goe_clip k b| <=
Num.ExtraDef.sqrtr 2 * k%:R * 3 ^+ k.-1 / d%:R * frobenius (a - b)

Statement as written in the source

Lemma goe_clip_lipschitz k (a b : 'rV[R]_(d * d)) :
  `|goe_clip k a - goe_clip k b| <=
  Num.sqrt 2 * k%:R * 3 ^+ k.-1 / d%:R * frobenius (a - b).

Used by 2 declarations in 1 file

this file: polyfun_goe_clip, goe_tr_var

lemma polyfun_goe_tr source, line 863

forall {R : realType} (d k : nat), polyfun (goe_tr k)

Statement as written in the source

Lemma polyfun_goe_tr k : polyfun (goe_tr k).

Used by 4 declarations in 2 files

this file: goe_clip_err2, goe_tr_var
GaussianAnalysis.random_matrix.wigner: goe_tr_cov_cvg, goe_clip_cvg

lemma goe_clip_bound source, line 869

forall {R : realType} [d : nat] (k : nat) (a : 'rV_(d * d)), `|goe_clip k a| <= 3 ^+ k

Statement as written in the source

Lemma goe_clip_bound k a : `|goe_clip k a| <= 3 ^+ k.

Used by 1 declaration in 1 file

this file: polyfun_goe_clip

lemma polyfun_goe_clip source, line 882

forall {R : realType} (d k : nat), polyfun (goe_clip k)

Statement as written in the source

Lemma polyfun_goe_clip k : polyfun (goe_clip k).

Used by 4 declarations in 2 files

this file: goe_clip_err2, goe_tr_var
GaussianAnalysis.random_matrix.wigner: goe_clip_cvg, goe_stat_clip_mean_cvg

lemma goe_clip_err2 source, line 892

forall {R : realType} [d : nat] (k : nat) [u : R],
(0 < d)%N ->
0 <= u ->
\int[gauss (d * d)]_a (goe_tr k a - goe_clip k a) ^+ 2 <=
4 * (k.*2)`!%:R *
expR (2 * Num.ExtraDef.sqrtr 2 * (2 * u + 1) + (2 * u + 1) ^+ 2 / d%:R - 6 * u)

E (t_k - goe_clip k)^2 <= 4 (2 k)! exp (2 sqrt 2 (2 u + 1) + (2 u + 1)^2 / d - 6 u) for every u >= 0.

Statement as written in the source

Lemma goe_clip_err2 k (u : R) : (0 < d)%N -> 0 <= u ->
  \int[gauss (d * d)]_a (goe_tr k a - goe_clip k a) ^+ 2 <=
  4 * (k.*2)`!%:R *
    expR (2 * Num.sqrt 2 * (2 * u + 1) + (2 * u + 1) ^+ 2 / d%:R - 6 * u).

Used by 1 declaration in 1 file

this file: goe_clip_err2_small

theorem goe_tr_var main result source, line 941

forall {R : realType} [d : nat] (k : nat) [u : R],
(0 < d)%N ->
0 <= u ->
\int[gauss (d * d)]_a (goe_tr k a - \int[gauss (d * d)]_b goe_tr k b) ^+ 2 <=
2 * (Num.ExtraDef.sqrtr 2 * k%:R * 3 ^+ k.-1 / d%:R) ^+ 2 +
8 * (k.*2)`!%:R *
expR (2 * Num.ExtraDef.sqrtr 2 * (2 * u + 1) + (2 * u + 1) ^+ 2 / d%:R - 6 * u)

Var t_k <= 2 L^2 + 8 (2 k)! exp (2 sqrt 2 (2 u + 1) + (2 u + 1)^2 / d - 6 u) for every u >= 0, with L = sqrt 2 k 3^(k-1) / d the Lipschitz constant of the clipped statistic: Var t_k <= E (t_k - E S)^2 <= 2 E (t_k - S)^2 + 2 Var S, Var S <= L^2 by the Gaussian Poincare inequality, and (t_k - S)^2 <= 4 (2 k)! exp ((2 u + 1) opnorm W - 6 u) by goe_clip_err.

Main result, as the README states it

Var (tr W^k / d) tends to 0, with the bound 2 L^2 + 8 (2k)! exp (2 sqrt 2 (2u + 1) + (2u + 1)^2 / d - 6u) for every u >= 0, L = sqrt 2 k 3^(k-1) / d: the statistic of the eigenvalues clipped to [-3, 3] is L-Lipschitz (Hoffman-Wielandt) and obeys the Gaussian Poincare inequality. |Cov (X, Y)| <= (Var X + Var Y) / 2.

Statement as written in the source

Theorem goe_tr_var k (u : R) : (0 < d)%N -> 0 <= u ->
  \int[gauss (d * d)]_a (goe_tr k a - \int[gauss (d * d)]_b goe_tr k b) ^+ 2 <=
  2 * (Num.sqrt 2 * k%:R * 3 ^+ k.-1 / d%:R) ^+ 2 +
  8 * (k.*2)`!%:R *
    expR (2 * Num.sqrt 2 * (2 * u + 1) + (2 * u + 1) ^+ 2 / d%:R - 6 * u).

Used by 1 declaration in 1 file

this file: goe_tr_var_small

sectiongoe_moments

Context {R : realType}.
Local Notation gauss := (@gauss R).

theorem goe_schwinger_dyson main result source, line 1018

forall {R : realType} (d k : nat),
\int[gauss (d * d)]_a \tr (goe_mx a ^+ k.+1) =
d%:R^-1 *
(k%:R * \int[gauss (d * d)]_a \tr (goe_mx a ^+ k.-1) +
 \sum_(r < k) \int[gauss (d * d)]_a (\tr (goe_mx a ^+ r) * \tr (goe_mx a ^+ (k.-1 - r))))

The Schwinger-Dyson equation for the moments of the GOE: E tr W^(k+1) = (k E tr W^(k-1) + \sum_(r < k) E[tr W^r tr W^(k-1-r)]) / d.

Main result

Stated in the README together with goe_mx.

Statement as written in the source

Theorem goe_schwinger_dyson d k :
  \int[gauss (d * d)]_a \tr (goe_mx a ^+ k.+1) =
  d%:R^-1 * (k%:R * \int[gauss (d * d)]_a \tr (goe_mx a ^+ k.-1) +
    \sum_(r < k) \int[gauss (d * d)]_a
      (\tr (goe_mx a ^+ r) * \tr (goe_mx a ^+ (k.-1 - r)))).

Used by 2 declarations in 2 files

this file: goe_tr_sd
GaussianAnalysis.random_matrix.wigner: goe_moment_cvg

sectiongoe_tr_moments

Context {R : realType} (d : nat).
Local Notation gauss := (@gauss R).

lemma goe_tr_sd main result source, line 1099

forall {R : realType} (d k : nat),
\int[gauss (d * d)]_a goe_tr k.+2 a =
k.+1%:R / d%:R * \int[gauss (d * d)]_a goe_tr k a +
\sum_(r < k.+1) \int[gauss (d * d)]_a (goe_tr r a * goe_tr (k - r) a)

The Schwinger-Dyson equation for t_k = tr W^k / d: E t_(k+2) = (k + 1) / d E t_k + \sum_(r <= k) E[t_r t_(k-r)].

Main result

Stated in the README together with goe_mx.

Statement as written in the source

Lemma goe_tr_sd k :
  \int[gauss (d * d)]_a goe_tr k.+2 a =
  k.+1%:R / d%:R * \int[gauss (d * d)]_a goe_tr k a +
  \sum_(r < k.+1) \int[gauss (d * d)]_a (goe_tr r a * goe_tr (k - r) a).

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.wigner: goe_moment_cvg

lemma goe_tr_var_small main result source, line 1120

forall {R : realType} (k : nat) [eps : R],
0 < eps ->
exists D : nat,
  forall d1 : nat,
  (D <= d1)%N ->
  \int[gauss (d1 * d1)]_a (goe_tr k a - \int[gauss (d1 * d1)]_b goe_tr k b) ^+ 2 <= eps

Var t_k tends to 0: for every eps > 0, Var t_k <= eps for every large d, by goe_tr_var with u chosen from eps and d >= (2 u + 1)^2.

Main result

Stated in the README together with goe_tr_var.

Statement as written in the source

Lemma goe_tr_var_small k (eps : R) : 0 < eps -> exists D : nat, forall d1,
  (D <= d1)%N ->
  \int[gauss (d1 * d1)]_a (goe_tr k a - \int[gauss (d1 * d1)]_b goe_tr k b) ^+ 2
    <= eps.

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.wigner: goe_tr_cov_cvg

lemma goe_clip_err2_small source, line 1189

forall {R : realType} (k : nat) [eps : R],
0 < eps ->
exists D : nat,
  forall d1 : nat,
  (D <= d1)%N -> \int[gauss (d1 * d1)]_a (goe_tr k a - goe_clip k a) ^+ 2 <= eps

E (t_k - goe_clip k)^2 tends to 0.

Statement as written in the source

Lemma goe_clip_err2_small k (eps : R) : 0 < eps -> exists D : nat, forall d1,
  (D <= d1)%N ->
  \int[gauss (d1 * d1)]_a (goe_tr k a - goe_clip k a) ^+ 2 <= eps.

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.wigner: goe_clip_cvg

lemma goe_opnorm_tail_small main result source, line 1227

forall {R : realType} [c eps : R],
2 * Num.ExtraDef.sqrtr 2 < c ->
0 < eps ->
exists D : nat,
  forall d1 : nat,
  (D <= d1)%N -> (gauss (d1 * d1) [set a | (c <= opnorm (goe_mx a))%R] <= eps%:E)%E

P(opnorm W >= c) tends to 0 for every c > 2 sqrt 2.

Main result

Stated in the README together with goe_opnorm_mean.

Statement as written in the source

Lemma goe_opnorm_tail_small (c eps : R) : 2 * Num.sqrt 2 < c -> 0 < eps ->
  exists D : nat, forall d1, (D <= d1)%N ->
  (gauss (d1 * d1) [set a | (c <= opnorm (goe_mx a))%R] <= eps%:E)%E.

Used by 2 declarations in 1 file

GaussianAnalysis.random_matrix.wigner: wigner, wigner_uniform

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.