Papers With

← All papers
First page of Poisson statistics for one-dimensional Anderson–Bernoulli Schrödinger operators

Poisson statistics for one-dimensional Anderson–Bernoulli Schrödinger operators

Yi Han

math-ph Oct 15, 2026 · v1 math.PR
formalization mathlib probability physics
Read PDF arXiv abstract Code
TL;DR
The main Poisson statistics theorem has an end-to-end Lean 4 formalization using Mathlib, checked by Lean's kernel and released as a public repository.
Abstract
We prove Poisson local eigenvalue statistics for one-dimensional Schrödinger operators with nondegenerate Bernoulli potentials at any fixed nonzero coupling. After unfolding by the integrated density of states (IDS), the local eigenvalue process converges to a Poisson point process of unit intensity at every energy in the interior of the almost-sure spectrum. The theorem also holds for bounded nonconstant iid potentials, provided the IDS is continuous and strictly increasing near the reference energy. If the IDS also has a finite positive derivative at that energy, the usual linear normalization gives the same limit. The proof uses a phase coordinate with exact IDS drift to obtain a uniform exponential crossing law and joint Poisson counts in disjoint energy windows.
Problem

The goal is Poisson local eigenvalue statistics for one-dimensional Anderson–Bernoulli Schrödinger operators at every fixed nonzero coupling. The atomic Bernoulli law blocks the classical Minami-estimate proof that works for potentials with bounded density.

Approach

The spectrum is unfolded by the integrated density of states (IDS), so no density of states is required. A phase coordinate with exact IDS drift yields a uniform exponential law for crossing times of coupled phase gaps. Renewal arguments with residual pinning give Poisson counts in a single energy window, and a block-subdivision argument gives asymptotic independence across disjoint windows. The proof of the main theorem is formalized end-to-end in Lean 4 with Mathlib, with GPT-6 credited as assisting the formalization.

Results

After IDS unfolding, the local eigenvalue process converges to a unit-intensity Poisson point process at every interior energy of the spectrum. The result also holds for bounded nonconstant iid potentials whose IDS is continuous and strictly increasing near the reference energy. Under linear normalization, the same limit holds when the IDS has a finite positive derivative.