Wigner semicircle law

wigner_semicircle

Submitter: Kim Morrison.

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

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

Informal solution: 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.

theorem declaration uses `sorry`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Ω:Type u_1inst✝¹:MeasurableSpace Ωμ:Measure Ωinst✝:IsProbabilityMeasure μX:ℕ → ℕ → Ω → ℝ_hX_meas:∀ (i j : ℕ), Measurable (X i j)_hX_indep:iIndepFun (fun ij => X (↑ij).1 (↑ij).2) μ_hX_iid:∀ (i j i' j' : ℕ), i ≤ j → i' ≤ j' → 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 ∂Measure.map (fun x => x / √↑n) (empiricalSpectralMeasureHerm ⋯)) atTop
          (𝓝 (∫ (x : ℝ), f x ∂semicircleLaw))
  sorryAll goals completed! 🐙

Solved by

Not yet solved.