High-dimensional and geometric probability

Probability in high dimension and on geometric objects: log-concave and uniform convex-body laws, isotropic constants, the KLS and thin-shell conjectures and their bounds, random matrices (singularity of Bernoulli matrices, Tracy–Widom limits), and random Euclidean optimization (Beardwood–Halton–Hammersley).

• Beardwood–Halton–Hammersley theorem
• Singularity of random Bernoulli matrices
• Suprema of selector and empirical processes
• Thin-shell conjecture
• Isotropic constant of log-concave laws
• Kannan–Lovász–Simonovits conjecture
• Wigner's semicircle law

TheoremJohnstone's Tracy–Widom limit#●ready to prove

Let q be the Hastings–McLeod solution of Painlevé II (q'' = s q + 2 q³ with q(s) · 2 √π s^{1/4} e^{(2/3) s^{3/2}} → 1 as s → ∞). Let n k, p k → ∞ with n k / p k → γ ≥ 1, and let X have independent standard Gaussian entries (Measure.pi of gaussianReal 0 1 over Fin (n k) × Fin (p k)). The largest eigenvalue of Xᵀ X is ℓ₁ = sup_{‖v‖ = 1} ‖X v‖². Then for every s, the function x ↦ q x + (x - s) q x ² is integrable on (s, ∞) and P((ℓ₁ - μ_k) / σ_k ≤ s) → F₁(s) = exp (-(1/2) ∫ₛ^∞ (q x + (x - s) q x ²) dx) with Johnstone's μ_k = (√(n - 1) + √p)² and σ_k = (√(n - 1) + √p) (1/√(n - 1) + 1/√p)^{1/3}.

MathlibExt.Probability.TracyWidomWanted.johnstone_largest_eigenvalue_tracyWidom · 19 lines

public theorem_wanted johnstone_largest_eigenvalue_tracyWidom
    (q : ℝ → ℝ) (hq : ContDiff ℝ 2 q)
    (hq_ode : ∀ s, deriv (deriv q) s = s * q s + 2 * q s ^ 3)
    (hq_airy : Tendsto (fun s => q s * (2 * Real.sqrt Real.pi * s ^ (1 / 4 : ℝ) *
      Real.exp (2 / 3 * s ^ (3 / 2 : ℝ)))) atTop (𝓝 1))
    (n p : ℕ → ℕ) (hn : Tendsto n atTop atTop) (hp : Tendsto p atTop atTop)
    (γ : ℝ) (hγ : 1 ≤ γ) (hratio : Tendsto (fun k => (n k : ℝ) / p k) atTop (𝓝 γ))
    (s : ℝ) :
    IntegrableOn (fun x => q x + (x - s) * q x ^ 2) (Set.Ioi s) ∧
      Tendsto (fun k =>
        (Measure.pi fun _ : Fin (n k) × Fin (p k) => gaussianReal 0 1)
          {X | ((⨆ v : {v : EuclideanSpace ℝ (Fin (p k)) // ‖v‖ = 1},
                ∑ i, (∑ j, X (i, j) * v.1 j) ^ 2) -
              (Real.sqrt ((n k : ℝ) - 1) + Real.sqrt (p k)) ^ 2) /
            ((Real.sqrt ((n k : ℝ) - 1) + Real.sqrt (p k)) *
              (1 / Real.sqrt ((n k : ℝ) - 1) + 1 / Real.sqrt (p k)) ^ (1 / 3 : ℝ)) ≤ s})
        atTop
        (𝓝 (ENNReal.ofReal
          (Real.exp (-(1 / 2) * ∫ x in Set.Ioi s, (q x + (x - s) * q x ^ 2)))))

Sources

• I. M. Johnstone, Ann. Statist. 29 (2001), 295–327, Theorem 1.1; Tracy–Widom (1996) for F₁; Hastings–McLeod (1980) for q.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.