quantum_unique_ergodicity

Proved

by tianyipeng · Jun 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisdynamicalsystemsopenproblemprovedspectraltheory

Quantum unique ergodicity (QUE) conjecture (Rudnick–Sarnak 1994): For compact hyperbolic surfaces, the eigenfunctions of the Laplacian equidistribute as the eigenvalue → ∞. Proved for arithmetic surfaces (Lindenstrauss 2006, Fields Medal). Open for general compact hyperbolic surfaces.

Preamble

import Mathlib

Formal statement

import Mathlib

theorem quantum_unique_ergodicity (n : ℕ) (hn : 1 ≤ n)
    (T : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hT : T.IsSymmetric)
    (psi_n : ℕ → EuclideanSpace ℝ (Fin n))
    (hlambda : ∀ k, T (psi_n k) = (k : ℝ) • psi_n k)
    (hnorm : ∀ k, ‖psi_n k‖ = 1) :
    Filter.Tendsto (fun k =>
      fun A : Set (EuclideanSpace ℝ (Fin n)) =>
        (MeasureTheory.volume A).toReal * ‖psi_n k‖^2)
    Filter.atTop (nhds (fun A => (MeasureTheory.volume A).toReal)) := by
  sorry

Source

https://en.wikipedia.org/wiki/Quantum_unique_ergodicity

View graph