Wigner semicircle law

wigner_semicircle — a formalization challenge from the lean-eval benchmark.

Notes

For an iid family X i j : Ω → ℝ of mean-0, variance-1 real random variables (parameterised over upper-triangular pairs i ≤ j), the empirical spectral measure of the real-symmetric matrix W_n / √n (with W_n(i, j) = X (min i j) (max i j)) converges weakly, almost surely, to the semicircle measure on [−2, 2] with density √(4 − x²) / (2π). Weak convergence is stated against bounded continuous test functions: almost surely ∫ f dμ_n → ∫ f dμ_∞ for every bounded continuous f. The hypotheses include Integrable (X i j) and Integrable ((X i j)^2) so the mean/variance identities are genuine (mathlib's Bochner integral defaults to 0 on non-integrable integrands). §102 of Knill's Some Fundamental Theorems in Mathematics.

Formal statement

/-- **Wigner's semicircle law** (Wigner 1955). For an iid family of
mean-`0`, variance-`1` real random variables, the empirical spectral
measure of the rescaled real-symmetric matrix `W_n / √n` converges
weakly, almost surely, to the semicircle measure on `[−2, 2]`. -/
theorem 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)) := by
  sorry

Informal solution sketch

Two main approaches: (i) the moment method, computing ∫ x^k dμ_n → ∫ x^k dμ_∞ for every k and matching the limit moments to the semicircle moments — odd moments vanish, the (2m)-th moment equals the Catalan number C_m, identified combinatorially via non-crossing pair partitions on 2m vertices; (ii) the Stieltjes-transform method, showing the Stieltjes transform s_n(z) of μ_n satisfies a fixed-point equation converging to the semicircle Stieltjes transform (the convention here: s(z) = ∫ (x − z)⁻¹ dμ(x) for Im z > 0, giving the unique root of s² + zs + 1 = 0 in the upper half plane). Mathlib has the spectral framework (Matrix.IsHermitian.eigenvalues), iid hypotheses (iIndepFun, IdentDistrib), and weak convergence on Polish spaces (Mathlib/MeasureTheory/Measure/Portmanteau.lean), but no semicircle measure, no Stieltjes transform, no Catalan-number combinatorics on non-crossing partitions, and no random-matrix universality framework.

Source

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: wigner_semicircle
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.