Papers With

← All papers
First page of Strict Dirichlet Pólya Inequality for Simply Connected Planar Domains

Strict Dirichlet Pólya Inequality for Simply Connected Planar Domains

Quanyu Tang, Zuoqin Wang

math.AP Oct 9, 2026 · v1 math.SP
formalization analysis ai-agents
Read PDF arXiv abstract Code
TL;DR
The main strict Dirichlet Pólya theorem and a strict Neumann analogue were formalized in Lean 4, assisted by Harmonic's Aristotle and OpenAI's Codex.
Abstract
We establish the strict Dirichlet Pólya inequality on every bounded simply connected planar domain. The proof uses a unitary boundary transport formulation of the Helmholtz equation and relates Dirichlet resonances to unitary eigenphase crossings through the Dirichlet-to-Neumann map. An exact area identity yields the sharp Weyl coefficient, while a Ky Fan estimate leaves a strictly positive remainder in the counting estimate. The general case follows by conformal exhaustion.
Problem

Pólya's conjecture asserts that Dirichlet eigenvalues of planar domains satisfy λ_j ≥ 4πj/|Ω|. The paper proves the strict version of this inequality for every bounded simply connected planar domain.

Approach

Boundary derivative jets of Dirichlet eigenfunctions are turned into a unitary boundary transport, built on the unilateral shift and its rank-one commutator. Dirichlet resonances are linked to unitary eigenphase crossings through the Dirichlet-to-Neumann map and a Cayley transform. An area identity for the trace of a positive radial generator gives the sharp Weyl coefficient. A Ky Fan estimate leaves a strictly positive remainder, and the general case follows by conformal exhaustion.

Results

The strict inequality |Ω|λ_j(Ω) > 4πj holds for all j ≥ 1 on bounded simply connected planar domains. This theorem and the strict Neumann Pólya inequality for simply connected Lipschitz domains were formalized in Lean 4.