Wigner's semicircle law

DefinitionEmpirical spectral measure of a Hermitian matrix#✓fully proved

Let \(W\) be a Hermitian \(n \times n\) complex matrix with real eigenvalues \(\lambda_1, \dots, \lambda_n\), listed with multiplicity. The empirical spectral measure of \(W\) is the measure \(\frac{1}{n} \sum_{j=1}^{n} \delta_{\lambda_j}\) on \(\mathbb{R}\), where \(\delta_\lambda\) is the Dirac measure at \(\lambda\); for \(n = 0\) it is the zero measure.

noncomputable def empiricalSpectralMeasureHerm {n : ℕ}
    {W : Matrix (Fin n) (Fin n) ℂ} (hW : W.IsHermitian) : Measure ℝ :=
  (n : ℝ≥0∞)⁻¹ • ∑ j : Fin n, Measure.dirac (hW.eigenvalues j)

Used by 1

Used byWigner's semicircle law

DefinitionSemicircle distribution#✓fully proved

The semicircle distribution is the measure \(\sigma\) on \(\mathbb{R}\) given by \(\sigma(A) = \int_{A \cap [-2, 2]} \frac{\sqrt{4 - x^2}}{2\pi} \, dx\) for every measurable set \(A \subseteq \mathbb{R}\).

Since \(\int_{-2}^{2} \sqrt{4 - x^2} \, dx = 2\pi\), it is a probability measure.

noncomputable def semicircleLaw : Measure ℝ :=
  (volume.restrict (Set.Icc (-2 : ℝ) 2)).withDensity
    (fun x => ENNReal.ofReal (Real.sqrt (4 - x ^ 2) / (2 * Real.pi)))

Used by 1

Used byWigner's semicircle law

DefinitionWigner matrix#✓fully proved

Let \(X_{ij} : \Omega \to \mathbb{R}\), for \(i, j \in \mathbb{N}\), be real functions on a set \(\Omega\). For \(n \in \mathbb{N}\) and \(\omega \in \Omega\), the Wigner matrix \(W_n(\omega)\) is the \(n \times n\) complex matrix, with rows and columns indexed by \(\{0, \dots, n - 1\}\), whose entry at \((i, j)\) is the real number \(X_{\min(i, j)\, \max(i, j)}(\omega)\). Only the \(X_{ij}\) with \(i \le j\) are used, and the matrix is real symmetric.

noncomputable def wignerMatrix {Ω : Type*} (X : ℕ → ℕ → Ω → ℝ) (n : ℕ)
    (ω : Ω) : Matrix (Fin n) (Fin n) ℂ :=
  fun i j => ((X (min (i : ℕ) j) (max (i : ℕ) j) ω : ℝ) : ℂ)

Used by 2

Used byWigner matrices are Hermitian · Wigner's semicircle law

LemmaWigner matrices are Hermitian#✓fully proved

For every family of real functions \(X_{ij} : \Omega \to \mathbb{R}\), \(i, j \in \mathbb{N}\), on a set \(\Omega\), every \(n \in \mathbb{N}\) and every \(\omega \in \Omega\), the Wigner matrix \(W_n(\omega)\) is Hermitian.

The matrix is in fact real symmetric: its entry at \((i, j)\) is the real number \(X_{\min(i, j)\, \max(i, j)}(\omega)\), and \(\min\) and \(\max\) are symmetric in their arguments.

lemma wignerMatrix_isHermitian {Ω : Type*} (X : ℕ → ℕ → Ω → ℝ) (n : ℕ)
    (ω : Ω) : (wignerMatrix X n ω).IsHermitian

Uses 1 · Used by 1

Statement usesWigner matrix

Used byWigner's semicircle law

TheoremWigner's semicircle law#●ready to prove

Let \((\Omega, \mu)\) be a probability space and let \(X_{ij} : \Omega \to \mathbb{R}\), for \(i, j \in \mathbb{N}\), be measurable functions. Suppose that the family \((X_{ij})_{i \le j}\) is mutually independent, that all \(X_{ij}\) with \(i \le j\) have the same distribution, and that for \(i \le j\) both \(X_{ij}\) and \(X_{ij}^2\) are integrable with \(\mathbb{E}[X_{ij}] = 0\) and \(\mathbb{E}[X_{ij}^2] = 1\). For \(n \in \mathbb{N}\) and \(\omega \in \Omega\), let \(W_n(\omega)\) be the Wigner matrix of \(X\) and let \(L_n(\omega)\) be the image of its empirical spectral measure under \(x \mapsto x / \sqrt{n}\) (for \(n \ge 1\), the empirical spectral measure of \(W_n(\omega) / \sqrt{n}\)). Then for \(\mu\)-almost every \(\omega\), every bounded continuous function \(f : \mathbb{R} \to \mathbb{R}\) satisfies

\[\int f \, dL_n(\omega) \to \int f \, d\sigma \quad (n \to \infty),\]

where \(\sigma\) is the semicircle distribution.

MathlibExt.Analysis.WignerSemicircleWanted.Analysis.WignerSemicircleProblem.wigner_semicircle · 21 lines

public theorem_wanted wigner_semicircle
    {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ]
    (X : ℕ → ℕ → Ω → ℝ)
    (_hX_meas : ∀ i j, Measurable (X i j))
    (_hX_indep : iIndepFun
      (fun ij : {p : ℕ × ℕ // p.1 ≤ p.2} => X ij.val.1 ij.val.2) μ)
    (_hX_iid : ∀ i j i' j', i ≤ j → i' ≤ j' →
      ProbabilityTheory.IdentDistrib (X i j) (X i' j') μ μ)
    (_hX_int : ∀ i j, i ≤ j → Integrable (X i j) μ)
    (_hX_sq_int : ∀ i j, i ≤ j → Integrable (fun ω => (X i j ω) ^ 2) μ)
    (_hX_mean : ∀ i j, i ≤ j → ∫ ω, X i j ω ∂μ = 0)
    (_hX_var : ∀ i j, i ≤ j → ∫ ω, (X i j ω) ^ 2 ∂μ = 1) :
    ∀ᵐ ω ∂μ,
      ∀ (f : ℝ → ℝ), Continuous f → (∃ M, ∀ x, ‖f x‖ ≤ M) →
        Tendsto
          (fun n : ℕ =>
            ∫ x, f x ∂ (empiricalSpectralMeasureHerm
              (wignerMatrix_isHermitian X n ω)).map
                (fun x : ℝ => x / Real.sqrt n))
          atTop (𝓝 (∫ x, f x ∂semicircleLaw))

Sources

• E. Wigner, 'Characteristic vectors of bordered matrices with infinite dimensions', Ann. of Math. (2) 62 (1955) 548–564 (Gaussian case). Pastur's universality extending to all variances with finite second moments: L. Pastur, 'On the spectrum of random matrices', Teor. Mat. Fiz. 10 (1972) 102–112. Listed as §102 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem wigner_semicircle of the lean-eval benchmark.

Uses 4

Statement usesEmpirical spectral measure of a Hermitian matrix · Semicircle distribution · Wigner matrix · Wigner matrices are Hermitian

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.