GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisrandom_matrixwigner

Wigner's semicircle law for the GOE

GaussianAnalysis.random_matrix.wignerlibrary/random_matrix/wigner.v1,129 lines33 lemmas and theorems, 3 definitionssource
Imports 11 library modules and 25 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.poly, mathcomp.algebra.matrix, 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.realfun, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Required by 4 files of the paper proofs

Let W = goe_mx a for a of law gauss (d * d) (random_matrix/goe.v). The empirical law of its eigenvalues spec W (matrix/von_neumann.v) converges in probability to the semicircle law of radius 2. This is the form of the semicircle law that Lemma 5.14 of Koehler and Sohn (arXiv 2608.27372, line 5905) cites from Anderson, Guionnet and Zeitouni. This file completes item G7 of phase 5.

Proved:

  • weierstrass_lipschitz: Weierstrass's approximation theorem on a compact interval for Lipschitz functions, by Bernstein polynomials (not in MathComp-Analysis 1.16): bernstein_lipschitz, |B_n f (x) - f x| <= L / (2 sqrt n) on [0, 1] for f L-Lipschitz, from the mean and the variance of the binomial law (bernstein_mean, bernstein_var).
  • segner: Segner's recurrence c_(n+1) = \sum_(i <= n) c_i c_(n-i) for a sequence with c_0 = 1 and (i + 2) c_(i+1) = (4 i + 2) c_i, by sums symmetric under i |-> n - i (the Catalan numbers, without generating functions).
  • semicircle_catalan: the moments m_k of semicircle_prob 2 satisfy the recursion of the Schwinger-Dyson equation of goe.v in the limit, m_(k+1) = \sum_(r < k) m_r m_(k-1-r), from segner and the moment recursion and the odd moments of semicircle_law.v.
  • goe_moment_cvg: for W = goe_mx a with a of law gauss (d * d), E tr W^k / d tends to the k-th moment of semicircle_prob 2 as d tends to infinity, by induction on k with goe_tr_sd of goe.v, whose covariance terms tend to 0 (goe_tr_cov_cvg, from goe_tr_var_small and Rintegral_cov_le); the same holds for the eigenvalues clipped to [-3, 3] (goe_clip_cvg).
  • wigner: Wigner's semicircle law. For f continuous and L-Lipschitz on [-3, 3], and eps > 0, P(|goe_stat f a - \int f dsigma| >= eps) <= eps for every large d, where goe_stat f a = (1 / d) \sum_i f (spec W 0 i) and sigma = semicircle_prob 2. Off the event opnorm W >= 3, whose probability tends to 0 (goe_opnorm_tail_small), the statistic is that of f o clip 3, which is Lipschitz (clip_comp_lipschitz); its mean tends to \int f dsigma by polynomial approximation on [-3, 3] (goe_stat_clip_mean_cvg, with goe_stat_poly_clip, semicircle_poly and semicircle_clip), and it concentrates around its mean (goe_stat_conc: goe_stat g is sqrt 2 L / d-Lipschitz in a, goe_stat_lipschitz).
  • wigner_uniform: the same uniformly over a family f_t, t in [t0, t1], of functions L-Lipschitz on [-3, 3] and L-Lipschitz in t on [-3, 3]: for every large d, the event that |goe_stat f_t a - \int f_t dsigma| >= eps for some t lies in a measurable event of probability at most eps. A grid of step eps / (3 (|L| + 1)) in t, wigner at each grid point, the union bound (Boole_inequality), and the event opnorm W >= 3 again; between grid points goe_stat_near and semicircle_near. Lemma 5.14 uses it for the functions (x - t)_+ and (x - t)_+^2.
  • wigner_uniform_inf: under the same hypotheses, with t0 <= t1, the infimum over t in [t0, t1] of goe_stat (f t) a converges in probability to the infimum over t of \int f_t dsigma: for every large d, the samples where the two differ by at least eps lie in a measurable event of probability at most eps. It follows from wigner_uniform at eps / 3, with inf_adherent; no minimum needs to be attained.
goe_stat f a(1 / d) \sum_i f (spec (goe_mx a) 0 i), the empirical mean of f over the spectrum of the GOE matrix goe_mx a

Main results

ResultsStatement
goe_moment_cvggoe_clip_cvgsegnersemicircle_catalan
E tr W^k / d tends to \int x^k d(semicircle_prob 2) for every k, by induction from the Schwinger-Dyson equation, whose covariance terms vanish in the limit; the semicircle moments satisfy the same recursion (Segner's recurrence for the Catalan numbers, proved from their ratio recurrence).
wignergoe_stat_clip_mean_cvggoe_stat_conc
Wigner's semicircle law: for f continuous and Lipschitz on [-3, 3] and eps > 0, P(|(1 / d) \sum_i f (spec W 0 i) - \int f d(semicircle_prob 2)| >= eps) <= eps for every large d.
wigner_uniformgoe_stat_nearsemicircle_near
Wigner's law uniformly over a family f_t, t in [t0, t1], of continuous functions that are L-Lipschitz on [-3, 3] and L-Lipschitz in t there: for every eps > 0 and every large d, the event that |(1 / d) \sum_i f_t (spec W 0 i) - \int f_t d(semicircle_prob 2)| >= eps for some t lies in a measurable event of probability at most eps.
wigner_uniform_inf
Under the hypotheses of wigner_uniform, with t0 <= t1: the infimum over t in [t0, t1] of goe_stat (f t) a converges in probability to the infimum over t of \int f_t d(semicircle_prob 2). For every eps > 0 and every large d, the samples where the two infima differ by at least eps lie in a measurable set of Gaussian probability at most eps. No minimum needs to be attained.
weierstrass_lipschitzbernstein_lipschitz
Weierstrass's approximation theorem for Lipschitz functions: if f is L-Lipschitz on [a, b], then for every eps > 0 some polynomial p satisfies |p.[x] - f x| <= eps on [a, b]. On [0, 1] the Bernstein polynomial of f of degree n >= 1 is within L / (2 sqrt n) of f.

Declarations36 exported

lemma, theoremdefinitioninstancelocal
sectionbernstein
Context {R : realType}.
definition bernstein_basis source, line 89
Type
forall {R : realType}, nat -> nat -> R -> R
Definition
Definition bernstein_basis (n k : nat) (x : R) : R :=
  'C(n, k)%:R * x ^+ k * (1 - x) ^+ (n - k).

The Bernstein basis C(n, k) x^k (1 - x)^(n - k).

Used by 8 declarations in 1 file
lemma bernstein_sum1 source, line 92 
forall {R : realType} (n : nat) (x : R), \sum_(k < n.+1) bernstein_basis n k x = 1
Statement as written in the source
Lemma bernstein_sum1 n x : \sum_(k < n.+1) bernstein_basis n k x = 1.
Used by 3 declarations in 1 file
lemma bernstein_shift source, line 101 
forall {R : realType} (g : nat -> R) (m : nat) (x : R),
\sum_(k < m.+2) g k * k%:R * bernstein_basis m.+1 k x =
m.+1%:R * x * \sum_(j < m.+1) g j.+1 * bernstein_basis m j x

k C(n + 1, k) = (n + 1) C(n, k - 1): the sums against k shift the degree.

Statement as written in the source
Lemma bernstein_shift (g : nat -> R) m x :
  \sum_(k < m.+2) g k * k%:R * bernstein_basis m.+1 k x =
  m.+1%:R * x * \sum_(j < m.+1) g j.+1 * bernstein_basis m j x.
Used by 2 declarations in 1 file
lemma bernstein_mean source, line 115 
forall {R : realType} (n : nat) (x : R),
\sum_(k < n.+1) k%:R * bernstein_basis n k x = n%:R * x

The mean and the variance of the binomial law.

Statement as written in the source
Lemma bernstein_mean n x :
  \sum_(k < n.+1) k%:R * bernstein_basis n k x = n%:R * x.
Used by 1 declaration in 1 file
lemma bernstein_var source, line 123 
forall {R : realType} (n : nat)
  (x : join_GRing_PzRing_between_Algebra_BaseZmodule_and_GRing_PzSemiRing R),
\sum_(k < n.+1) (k%:R - n%:R * x) ^+ 2 * bernstein_basis n k x = n%:R * x * (1 - x)
Statement as written in the source
Lemma bernstein_var n x :
  \sum_(k < n.+1) (k%:R - n%:R * x) ^+ 2 * bernstein_basis n k x =
  n%:R * x * (1 - x).
Used by 1 declaration in 1 file
lemma bernstein_basis_ge0 source, line 142 
forall {R : realType} (n k : nat)
  [x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R],
0 <= x <= 1 -> 0 <= bernstein_basis n k x
Statement as written in the source
Lemma bernstein_basis_ge0 n k x : 0 <= x <= 1 -> 0 <= bernstein_basis n k x.
Used by 1 declaration in 1 file
definition bernstein source, line 149
Type
forall {R : realType}, (R -> R) -> nat -> R -> R
Definition
Definition bernstein (f : R -> R) n (x : R) : R :=
  \sum_(k < n.+1) f (k%:R / n%:R) * bernstein_basis n k x.

The Bernstein polynomial of f of degree n.

Used by 2 declarations in 1 file
lemma bernstein_lipschitz main result source, line 154 
forall {R : realType} [f : R -> R] [L : R] (n : nat)
  [x : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R],
(forall y z : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R,
 0 <= y <= 1 -> 0 <= z <= 1 -> `|f y - f z| <= L * `|y - z|) ->
0 <= x <= 1 -> `|bernstein f n.+1 x - f x| <= L / (2 * Num.ExtraDef.sqrtr n.+1%:R)

For f L-Lipschitz on [0, 1], the Bernstein polynomial of degree n.+1 is within L / (2 sqrt (n + 1)) of f on [0, 1].

Main result

Stated in the README together with weierstrass_lipschitz.

Statement as written in the source
Lemma bernstein_lipschitz (f : R -> R) (L : R) n x :
  (forall y z, 0 <= y <= 1 -> 0 <= z <= 1 -> `|f y - f z| <= L * `|y - z|) ->
  0 <= x <= 1 ->
  `|bernstein f n.+1 x - f x| <= L / (2 * Num.sqrt n.+1%:R).
Used by 1 declaration in 1 file
lemma bernstein_polyE source, line 216 
forall {R : realType} (f : R -> R) (n : nat),
exists p : {poly R}, forall x : R, bernstein f n x = p.[x]

The Bernstein polynomial is a polynomial.

Statement as written in the source
Lemma bernstein_polyE (f : R -> R) n : exists p : {poly R},
  forall x, bernstein f n x = p.[x].
Used by 1 declaration in 1 file
theorem weierstrass_lipschitz main result source, line 227 
forall {R : realType} [f : R -> R] [L a b eps : R],
a < b ->
0 < eps ->
(forall y z : R, a <= y <= b -> a <= z <= b -> `|f y - f z| <= L * `|y - z|) ->
exists p : {poly R}, forall x : R, a <= x <= b -> `|p.[x] - f x| <= eps

Weierstrass's approximation theorem for Lipschitz functions on a compact interval, with an explicit degree.

Main result, as the README states it

Weierstrass's approximation theorem for Lipschitz functions: if f is L-Lipschitz on [a, b], then for every eps > 0 some polynomial p satisfies |p.[x] - f x| <= eps on [a, b]. On [0, 1] the Bernstein polynomial of f of degree n >= 1 is within L / (2 sqrt n) of f.

Statement as written in the source
Theorem weierstrass_lipschitz (f : R -> R) (L a b eps : R) :
  a < b -> 0 < eps ->
  (forall y z, a <= y <= b -> a <= z <= b -> `|f y - f z| <= L * `|y - z|) ->
  exists p : {poly R}, forall x, a <= x <= b -> `|p.[x] - f x| <= eps.
Used by 1 declaration in 1 file
sectioncatalan
Context {R : realFieldType}.
lemma segner main result source, line 279 
forall {R : realFieldType} [c : nat -> R],
c 0%N = 1 ->
(forall i : nat, i.+2%:R * c i.+1 = (4 * i%:R + 2) * c i) ->
forall n : nat, \sum_(0 <= i < n.+1) c i * c (n - i)%N = c n.+1

Segner's recurrence c_(n+1) = \sum_(i <= n) c_i c_(n-i) for a sequence with c_0 = 1 and (i + 2) c_(i+1) = (4 i + 2) c_i, such as the Catalan numbers and the even moments of the semicircle law of radius 2.

Main result

Stated in the README together with goe_moment_cvg.

Statement as written in the source
Lemma segner (c : nat -> R) : c 0%N = 1 ->
  (forall i, i.+2%:R * c i.+1 = (4 * i%:R + 2) * c i) ->
  forall n, \sum_(0 <= i < n.+1) c i * c (n - i)%N = c n.+1.
Used by 1 declaration in 1 file
sectionsemicircle_catalan
Context {R : realType}.
Local Notation m k := (\int[semicircle_prob (2 : R)]_x ((x : R) ^+ k)).
lemma sum_parity source, line 325 
forall {R : realType} (f : nat -> R) (n : nat),
\sum_(r < n.*2.+1) f r = \sum_(i < n.+1) f i.*2 + \sum_(i < n) f i.*2.+1

A sum over r < 2 n + 1, split into even and odd r.

Statement as written in the source
Lemma sum_parity (f : nat -> R) n :
  \sum_(r < n.*2.+1) f r =
  \sum_(i < n.+1) f i.*2 + \sum_(i < n) f i.*2.+1.
Used by 1 declaration in 1 file
lemma semicircle_catalan main result source, line 338 
forall {R : realType} (k : nat),
\int[semicircle_prob (2 : R)]_x (x : R) ^+ k.+1 =
\sum_(r < k)
   \int[semicircle_prob (2 : R)]_x (x : R) ^+ r *
   \int[semicircle_prob (2 : R)]_x (x : R) ^+ (k.-1 - r)

The moments of the semicircle law of radius 2 satisfy the recursion of the Schwinger-Dyson equation: m_(k+1) = \sum_(r < k) m_r m_(k-1-r).

Main result

Stated in the README together with goe_moment_cvg.

Statement as written in the source
Lemma semicircle_catalan k : m k.+1 = \sum_(r < k) m r * m (k.-1 - r)%N.
Used by 1 declaration in 1 file
sectiongoe_moment_limit
Context {R : realType}.
Local Notation m k := (\int[semicircle_prob (2 : R)]_x ((x : R) ^+ k)).
lemma cvg_nat_eps source, line 379 
forall {R : realType} [u : nat -> R] [l : R],
(forall eps : R, 0 < eps -> exists D : nat, forall d : nat, (D <= d)%N -> `|l - u d| <= eps) ->
u x @[x --> \oo] --> l
Statement as written in the source
Lemma cvg_nat_eps (u : nat -> R) (l : R) :
  (forall eps : R, 0 < eps ->
     exists D, forall d, (D <= d)%N -> `|l - u d| <= eps) ->
  u @ \oo --> l.
Used by 4 declarations in 1 file
lemma cvg_sum_seq source, line 388 
forall {R : realType} [I : Type] [s : seq I] [f : I -> nat -> R] [l : I -> R],
(forall i : I, f i x @[x --> \oo] --> l i) ->
\sum_(i <- s) f i d @[d --> \oo] --> \sum_(i <- s) l i
Statement as written in the source
Lemma cvg_sum_seq (I : Type) (s : seq I) (f : I -> nat -> R) (l : I -> R) :
  (forall i, f i @ \oo --> l i) ->
  (fun d => \sum_(i <- s) f i d) @ \oo --> \sum_(i <- s) l i.
Used by 2 declarations in 1 file
lemma goe_tr_cov_cvg source, line 398 
forall {R : realType} (r q : nat),
\int[gauss (d * d)]_a (goe_tr r a * goe_tr q a) -
\int[gauss (d * d)]_a goe_tr r a * \int[gauss (d * d)]_a goe_tr q a @[d --> \oo] --> 0

The covariances of the normalized traces tend to 0.

Statement as written in the source
Lemma goe_tr_cov_cvg r q :
  (fun d => \int[@gauss R (d * d)]_a (goe_tr r a * goe_tr q a) -
    \int[@gauss R (d * d)]_a goe_tr r a * \int[@gauss R (d * d)]_a goe_tr q a)
  @ \oo --> 0.
Used by 1 declaration in 1 file
theorem goe_moment_cvg main result source, line 414 
forall {R : realType} [k : nat],
\int[gauss (d * d)]_a goe_tr k a @[d --> \oo] --> \int[semicircle_prob (2 : R)]_x
                                                     (x : R) ^+ k

Wigner's moment limit: E tr W^k / d tends to the k-th moment of the semicircle law of radius 2.

Main result, as the README states it

E tr W^k / d tends to \int x^k d(semicircle_prob 2) for every k, by induction from the Schwinger-Dyson equation, whose covariance terms vanish in the limit; the semicircle moments satisfy the same recursion (Segner's recurrence for the Catalan numbers, proved from their ratio recurrence).

Statement as written in the source
Theorem goe_moment_cvg k :
  (fun d => \int[@gauss R (d * d)]_a goe_tr k a) @ \oo --> m k.
Used by 1 declaration in 1 file
lemma goe_clip_cvg main result source, line 471 
forall {R : realType} [j : nat],
\int[gauss (d * d)]_a goe_clip j a @[d --> \oo] --> \int[semicircle_prob (2 : R)]_x
                                                       (x : R) ^+ j

The moments of the eigenvalues clipped to [-3, 3] have the same limits.

Main result

Stated in the README together with goe_moment_cvg.

Statement as written in the source
Lemma goe_clip_cvg j :
  (fun d => \int[@gauss R (d * d)]_a goe_clip j a) @ \oo --> m j.
Used by 1 declaration in 1 file
sectionwigner
Context {R : realType}.
Local Notation sigma := (semicircle_prob (2 : R)).
Local Notation m k := (\int[sigma]_x ((x : R) ^+ k)).
definition goe_stat source, line 512
Type
forall {R : realType} [d : nat], (R -> R) -> 'rV_(d * d) -> R
Definition
Definition goe_stat d (f : R -> R) (a : 'rV[R]_(d * d)) : R :=
  (\sum_i f (spec (goe_mx a) 0 i)) / d%:R.

The empirical mean (1 / d) \sum_i f (lambda_i) of f over the spectrum of W = goe_mx a.

Used by 10 declarations in 1 file
lemma goe_stat_poly_clip source, line 515 
forall {R : realType} [d : nat] (p : {poly R}) (a : 'rV_(d * d)),
goe_stat (fun x : R => p.[clip 3 x]) a = \sum_(j < size p) p`_j * goe_clip j a
Statement as written in the source
Lemma goe_stat_poly_clip d (p : {poly R}) (a : 'rV[R]_(d * d)) :
  goe_stat (fun x => p.[clip 3 x]) a =
  \sum_(j < size p) p`_j * goe_clip j a.
Used by 1 declaration in 1 file
lemma integrable_semicircle_poly source, line 524 
forall {R : realType} (p : {poly R}),
(semicircle_prob (2 : R)).-integrable [set: R] (EFin \o horner p)
Statement as written in the source
Lemma integrable_semicircle_poly (p : {poly R}) :
  sigma.-integrable [set: R] (EFin \o horner p).
lemma semicircle_poly source, line 531 
forall {R : realType} (p : {poly R}),
\int[semicircle_prob (2 : R)]_x p.[x] =
\sum_(j < size p) p`_j * \int[semicircle_prob (2 : R)]_x (x : R) ^+ j
Statement as written in the source
Lemma semicircle_poly (p : {poly R}) :
  \int[sigma]_x p.[x] = \sum_(j < size p) p`_j * m j.
Used by 1 declaration in 1 file
lemma continuous_clip source, line 545 
forall {R : realType} [c : R], continuous (clip c)
Statement as written in the source
Lemma continuous_clip (c : R) : continuous (clip c).
Used by 4 declarations in 1 file
lemma semicircle_clip source, line 553 
forall {R : realType} [h : R -> R],
continuous h ->
\int[semicircle_prob (2 : R)]_x h (clip 3 x) = \int[semicircle_prob (2 : R)]_x h x

The semicircle law of radius 2 lives on [-2, 2]: clipping at 3 does not change its integrals.

Statement as written in the source
Lemma semicircle_clip (h : R -> R) : continuous h ->
  \int[sigma]_x h (clip 3 x) = \int[sigma]_x h x.
Used by 2 declarations in 1 file
lemma goe_stat_lipschitz source, line 566 
forall {R : realType} [d : nat] [g : R -> R] [L : R],
0 <= L ->
(forall x y : R, `|g x - g y| <= L * `|x - y|) ->
forall a b : 'rV_(d * d),
`|goe_stat g a - goe_stat g b| <= Num.ExtraDef.sqrtr 2 * L / d%:R * frobenius (a - b)

For g L-Lipschitz, goe_stat g is (sqrt 2 L / d)-Lipschitz in a.

Statement as written in the source
Lemma goe_stat_lipschitz d (g : R -> R) (L : R) : 0 <= L ->
  (forall x y, `|g x - g y| <= L * `|x - y|) ->
  forall a b : 'rV[R]_(d * d),
  `|goe_stat g a - goe_stat g b| <= Num.sqrt 2 * L / d%:R * frobenius (a - b).
Used by 2 declarations in 1 file
lemma clip_comp_lipschitz source, line 588 
forall {R : realType} [f : R -> R] [L : R],
(forall x y : R, -3 <= x <= 3 -> -3 <= y <= 3 -> `|f x - f y| <= L * `|x - y|) ->
0 <= L /\ (forall x y : R, `|f (clip 3 x) - f (clip 3 y)| <= L * `|x - y|)

A test function that is L-Lipschitz on [-3, 3], composed with clip 3, is L-Lipschitz and bounded.

Statement as written in the source
Lemma clip_comp_lipschitz (f : R -> R) (L : R) :
  (forall x y : R, -3 <= x <= 3 -> -3 <= y <= 3 -> `|f x - f y| <= L * `|x - y|) ->
  0 <= L /\ forall x y : R, `|f (clip 3 x) - f (clip 3 y)| <= L * `|x - y|.
Used by 3 declarations in 1 file
lemma polyfun_goe_stat_clip source, line 602 
forall {R : realType} (d : nat) [f : R -> R] [L : R],
(forall x y : R, -3 <= x <= 3 -> -3 <= y <= 3 -> `|f x - f y| <= L * `|x - y|) ->
polyfun (goe_stat (fun x : R => f (clip 3 x)))
Statement as written in the source
Lemma polyfun_goe_stat_clip d (f : R -> R) (L : R) :
  (forall x y : R, -3 <= x <= 3 -> -3 <= y <= 3 -> `|f x - f y| <= L * `|x - y|) ->
  polyfun (@goe_stat d (fun x => f (clip 3 x))).
Used by 1 declaration in 1 file
theorem goe_stat_clip_mean_cvg main result source, line 634 
forall {R : realType} [f : R -> R] [L : R],
continuous f ->
(forall x y : R, -3 <= x <= 3 -> -3 <= y <= 3 -> `|f x - f y| <= L * `|x - y|) ->
\int[gauss (d * d)]_a goe_stat (fun x : R => f (clip 3 x)) a @[d --> \oo] --> 
\int[semicircle_prob (2 : R)]_x f x

The mean of the statistic of f o clip 3 tends to \int f dsigma, for f continuous and Lipschitz on [-3, 3]: by a polynomial p within eta of f on [-3, 3] (weierstrass_lipschitz), whose statistic is a combination of the clipped moments (goe_stat_poly_clip, goe_clip_cvg).

Main result

Stated in the README together with wigner.

Statement as written in the source
Theorem goe_stat_clip_mean_cvg (f : R -> R) (L : R) : continuous f ->
  (forall x y : R, -3 <= x <= 3 -> -3 <= y <= 3 -> `|f x - f y| <= L * `|x - y|) ->
  (fun d => \int[@gauss R (d * d)]_a goe_stat (fun x => f (clip 3 x)) a) @ \oo
    --> \int[sigma]_x f x.
Used by 1 declaration in 1 file
lemma goe_stat_conc main result source, line 740 
forall {R : realType} [g : R -> R] [L u eps : R],
0 <= L ->
(forall x y : R, `|g x - g y| <= L * `|x - y|) ->
0 < u ->
0 < eps ->
exists D : nat,
  forall d : nat,
  (D <= d)%N ->
  (gauss (d * d) [set a | (u <= `|goe_stat g a - \int[gauss (d * d)]_b goe_stat g b|)%R] <=
   eps%:E)%E

Concentration: for g L-Lipschitz, P(|goe_stat g - E goe_stat g| >= u) <= eps for every large d (gauss_concentration_abs_tail with the constant sqrt 2 (L + 1) / d).

Main result

Stated in the README together with wigner.

Statement as written in the source
Lemma goe_stat_conc (g : R -> R) (L u eps : R) : 0 <= L ->
  (forall x y, `|g x - g y| <= L * `|x - y|) -> 0 < u -> 0 < eps ->
  exists D : nat, forall d, (D <= d)%N ->
  (@gauss R (d * d) [set a | (u <= `|goe_stat g a -
     \int[@gauss R (d * d)]_b goe_stat g b|)%R] <= eps%:E)%E.
Used by 1 declaration in 1 file
lemma continuous_goe_stat source, line 785 
forall {R : realType} [d : nat] [f : R -> R], continuous f -> continuous (goe_stat f)
Statement as written in the source
Lemma continuous_goe_stat d (f : R -> R) : continuous f ->
  continuous (@goe_stat d f).
Used by 2 declarations in 1 file
theorem wigner main result source, line 806 
forall {R : realType} [f : R -> R] [L : R],
continuous f ->
(forall x y : R, -3 <= x <= 3 -> -3 <= y <= 3 -> `|f x - f y| <= L * `|x - y|) ->
forall [eps : R],
0 < eps ->
exists D : nat,
  forall d : nat,
  (D <= d)%N ->
  (gauss (d * d) [set a | (eps <= `|goe_stat f a - \int[semicircle_prob (2 : R)]_x f x|)%R] <=
   eps%:E)%E

Wigner's semicircle law: for f continuous and Lipschitz on [-3, 3] and eps > 0, the probability that (1 / d) \sum_i f (lambda_i (W)) is farther than eps from \int f d(semicircle_prob 2) is at most eps for every large d.

Main result, as the README states it

Wigner's semicircle law: for f continuous and Lipschitz on [-3, 3] and eps > 0, P(|(1 / d) \sum_i f (spec W 0 i) - \int f d(semicircle_prob 2)| >= eps) <= eps for every large d.

Statement as written in the source
Theorem wigner (f : R -> R) (L : R) : continuous f ->
  (forall x y : R, -3 <= x <= 3 -> -3 <= y <= 3 -> `|f x - f y| <= L * `|x - y|) ->
  forall eps : R, 0 < eps -> exists D : nat, forall d, (D <= d)%N ->
  (@gauss R (d * d) [set a | (eps <= `|goe_stat f a - \int[sigma]_x f x|)%R]
     <= eps%:E)%E.
Used by 1 declaration in 1 file
lemma goe_stat_near main result source, line 875 
forall {R : realType} [d : nat] [g h : R -> R] [c : R] [a : 'rV_(d * d)],
opnorm (goe_mx a) <= 3 ->
(forall x : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R,
 -3 <= x <= 3 -> `|g x - h x| <= c) ->
`|goe_stat g a - goe_stat h a| <= c

If |g x - h x| <= c on [-3, 3] and the spectrum of goe_mx a lies in [-3, 3], the statistics of g and h differ by at most c.

Main result

Stated in the README together with wigner_uniform.

Statement as written in the source
Lemma goe_stat_near d (g h : R -> R) (c : R) (a : 'rV[R]_(d * d)) :
  opnorm (goe_mx a) <= 3 -> (forall x, -3 <= x <= 3 -> `|g x - h x| <= c) ->
  `|goe_stat g a - goe_stat h a| <= c.
Used by 1 declaration in 1 file
lemma clip3_bound source, line 897 
forall {R : realType} (x : R), -3 <= clip 3 x <= 3
Statement as written in the source
Lemma clip3_bound (x : R) : -3 <= clip 3 x <= 3.
Used by 1 declaration in 1 file
lemma semicircle_near main result source, line 901 
forall {R : realType} [g h : R -> R] [c : R],
continuous g ->
continuous h ->
(forall x : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R,
 -3 <= x <= 3 -> `|g x - h x| <= c) ->
`|\int[semicircle_prob (2 : R)]_x g x - \int[semicircle_prob (2 : R)]_x h x| <= c

The same for the integrals against the semicircle law.

Main result

Stated in the README together with wigner_uniform.

Statement as written in the source
Lemma semicircle_near (g h : R -> R) (c : R) : continuous g -> continuous h ->
  (forall x, -3 <= x <= 3 -> `|g x - h x| <= c) ->
  `|\int[sigma]_x g x - \int[sigma]_x h x| <= c.
Used by 2 declarations in 1 file
theorem wigner_uniform main result source, line 933 
forall {R : realType} [f : R -> R -> R] [L t0 t1 : R],
(forall t : R, continuous (f t)) ->
(forall (t : R)
   (x y : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R),
 t0 <= t <= t1 -> -3 <= x <= 3 -> -3 <= y <= 3 -> `|f t x - f t y| <= L * `|x - y|) ->
(forall (t s : R)
   (x : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R),
 t0 <= t <= t1 -> t0 <= s <= t1 -> -3 <= x <= 3 -> `|f t x - f s x| <= L * `|t - s|) ->
forall [eps : R],
0 < eps ->
exists D : nat,
  forall d : nat,
  (D <= d)%N ->
  exists A : set 'rV_(d * d),
    [/\ (measure_matrix_display default_measure_display).-measurable A,
        (gauss (d * d) A <= eps%:E)%E
      & [set a | (exists2 t : R,
                    t0 <= t <= t1 &
                    eps <= `|goe_stat (f t) a - \int[semicircle_prob (2 : R)]_x f t x|)]
        `<=` A]

Wigner's law uniformly over a family f_t, t in [t0, t1], of functions that are L-Lipschitz on [-3, 3] and L-Lipschitz in t: for every large d, the event that some t has a deviation at least eps lies in a measurable event of probability at most eps. Lemma 5.14 of Koehler and Sohn uses it for (x - t)_+ and (x - t)_+^2.

Main result, as the README states it

Wigner's law uniformly over a family f_t, t in [t0, t1], of continuous functions that are L-Lipschitz on [-3, 3] and L-Lipschitz in t there: for every eps > 0 and every large d, the event that |(1 / d) \sum_i f_t (spec W 0 i) - \int f_t d(semicircle_prob 2)| >= eps for some t lies in a measurable event of probability at most eps.

Statement as written in the source
Theorem wigner_uniform (f : R -> R -> R) (L t0 t1 : R) :
  (forall t, continuous (f t)) ->
  (forall t x y, t0 <= t <= t1 -> -3 <= x <= 3 -> -3 <= y <= 3 ->
     `|f t x - f t y| <= L * `|x - y|) ->
  (forall t s x, t0 <= t <= t1 -> t0 <= s <= t1 -> -3 <= x <= 3 ->
     `|f t x - f s x| <= L * `|t - s|) ->
  forall eps : R, 0 < eps -> exists D : nat, forall d, (D <= d)%N ->
  exists A : set 'rV[R]_(d * d), [/\ measurable A,
    (@gauss R (d * d) A <= eps%:E)%E &
    [set a | exists2 t, t0 <= t <= t1 &
       eps <= `|goe_stat (f t) a - \int[sigma]_x f t x|] `<=` A].
Used by 1 declaration in 1 file
theorem wigner_uniform_inf main result source, line 1068 
forall {R : realType} [f : R -> R -> R] [L t0 t1 : R],
t0 <= t1 ->
(forall t : R, continuous (f t)) ->
(forall (t : R)
   (x y : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R),
 t0 <= t <= t1 -> -3 <= x <= 3 -> -3 <= y <= 3 -> `|f t x - f t y| <= L * `|x - y|) ->
(forall (t s : R)
   (x : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R),
 t0 <= t <= t1 -> t0 <= s <= t1 -> -3 <= x <= 3 -> `|f t x - f s x| <= L * `|t - s|) ->
forall [eps : R],
0 < eps ->
exists D : nat,
  forall d : nat,
  (D <= d)%N ->
  exists A : set 'rV_(d * d),
    [/\ (measure_matrix_display default_measure_display).-measurable A,
        (gauss (d * d) A <= eps%:E)%E
      & [set a | eps <=
                 `|inf [set goe_stat (f t) a | t in [set t | t0 <= t <= t1]] -
                   inf
                     [set \int[semicircle_prob (2 : R)]_x f t x
                        | t in [set t | t0 <= t <= t1]]|]
        `<=` A]

The minimum over t in [t0, t1], written as an infimum, of goe_stat (f t) converges in probability to the minimum over t of \int f t dsigma, under the hypotheses of wigner_uniform: outside an event of probability at most eps / 3, every goe_stat (f t) is within eps / 3 of its limit, so the two infima differ by less than 2 eps / 3. No minimum needs to be attained.

Main result, as the README states it

Under the hypotheses of wigner_uniform, with t0 <= t1: the infimum over t in [t0, t1] of goe_stat (f t) a converges in probability to the infimum over t of \int f_t d(semicircle_prob 2). For every eps > 0 and every large d, the samples where the two infima differ by at least eps lie in a measurable set of Gaussian probability at most eps. No minimum needs to be attained.

Statement as written in the source
Theorem wigner_uniform_inf (f : R -> R -> R) (L t0 t1 : R) : t0 <= t1 ->
  (forall t, continuous (f t)) ->
  (forall t x y, t0 <= t <= t1 -> -3 <= x <= 3 -> -3 <= y <= 3 ->
     `|f t x - f t y| <= L * `|x - y|) ->
  (forall t s x, t0 <= t <= t1 -> t0 <= s <= t1 -> -3 <= x <= 3 ->
     `|f t x - f s x| <= L * `|t - s|) ->
  forall eps : R, 0 < eps -> exists D : nat, forall d, (D <= d)%N ->
  exists A : set 'rV[R]_(d * d), [/\ measurable A,
    (@gauss R (d * d) A <= eps%:E)%E &
    [set a | eps <=
       `|inf [set goe_stat (f t) a | t in [set t | t0 <= t <= t1]] -
         inf [set \int[sigma]_x f t x | t in [set t | t0 <= t <= t1]]|]
    `<=` A].
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.