Proving theorems with Mathematica: Pólya’s conjecture and beyond

Michael Levitin, University of Reading and UCL
m.levitin@reading.ac.uk
michaellevitin.net

(RowDefault[, (Spacer1), , (Spacer1), ])  #WolframTechConf

Pólya’s conjecture

Let  be a bounded domain in , . We consider two boundary-value spectral problems in  for the Laplace operator,

,    ,

with either

(the Dirichlet condition)       or           (the Neumann condition).

In both cases, we have discrete spectra of real eigenvalues (i.e., the values of  for which a non-trivial solution  exists):

.

Finding eigenvalues analytically is only possible for very simple domains (e.g. boxes), and numerically  one can find only a limited number of eigenvalues reliably using, say, FEM. The main questions of my field, Spectral Geometry, are about relations between the shapes of domains and their eigenvalues (= the frequencies of their fundamental tones and overtones), e.g. “Can one hear the shape of a drum?”

We count the eigenvalues below a given value of using the counting functions

.

It is well known that for large  both counting functions behave asymptotically as

,

where the explicit constant  depends only on dimension , for example . The asymptotic formulae (1) are know as Weyl’s Law.

The famous conjecture (1954) of George Pólya is that

for all domains  and all parameter values , see example for a 3d-ball in the image.

Pólya himself proved (2) for tiling domains  (such that the whole space  can be filled without gaps by non-intersecting copies of ), for example boxes or triangles, but (2) remains open in full generality. Until last year, it was open even for the disk: obviously disks do not tile the plane. In the case of a disk and higher-dimensional balls, as well as in some similar cases, e.g. for sectors and annuli,  Pólya’s conjecture has been proved in a series of recent papers by N. Filonov, M. Levitin, I. Polterovich, and D. A. Sher [Invent. Math.; J. Spectral Theory; SIAM J. Math. Anal.; + work in progress, 2023-2024].

Bessel phases and zeros

For the disk, the eigenvalues of the Dirichlet and Neumann Laplacians can be obtained by separation of variables:

BesselJZero[n,m]^2, 
 (m^th) positive zero squared of D[BesselJ[n,z],z],
	except that ,

so that

.

It is however impossible to arrange these double-indexed sequences in an increasing order, and therefore count the zeros below a given  so we need to know a priori something about Bessel zeros.

Just calculating (or even getting good bounds for) large zeros of Bessel functions  of large order is not always straightforward:

TimeConstrained[BesselJZero[100000,50000]//N,10]

We introduce instead the Bessel phase functions

ArcTan[BesselY[ν,x]/BesselJ[ν,x]],          
 ArcTan[D[BesselY[ν,x],x]/D[BesselJ[ν,x],x]],

Leaving aside the question of how effectively one can compute these phase functions (tricky for large  and ), we derive good two-sided bounds for phase functions  in terms of some elementary functions (with some very involved intermediate calculations being Mathematica-assisted: for example at some stage we needed to to change variables in some parameter-dependent polynomials of degree 18 and may not have managed to do this by hand).

As the zeros of Bessel functions can be expressed in terms of inverse functions of the phases, e.g.

bounds for phases give (almost) elementary bounds for zeros.

A similar approach works for the zeros of Bessel derivatives.

The accuracy and range of applicability of our bounds are in almost all cases better than all earlier results: the contour plot shows the logarithm of the maximal relative error of bounds for  depending on  and .

Counting lattice points

Once we have the bounds on Bessel zeros, we reduce the proof of Pólya’s conjecture for disks, balls, and annuli to the following number-theoretical problem: we need to count (with some weights)  the number of lattice points under the graph of a monotone nonnegative function. Specifically for disks, let  be a given function, and let

Taking a particular function

,

we need to prove that

for all

We prove the lower bound in (3) analytically, but our proof of the upper bound leaves a finite gap in the range of  where the proof is not sharp enough. We close the gap with the help of a computer-assisted algorithm realised in Mathematica and satisfying two essential principles:

the algorithm should converge in a finite number of steps

all calculations should be exact, avoiding any floating-point approximations

We achieve the second goal with the help of what we call verified rational approximations of square roots, inverse trigonometric functions, etc.:  in essence creating one-sided (above or below) versions of Mathematica’s Rationalize[] command but with rigorous verification of inequalities for transcendental functions.

For higher-dimensional balls and for annuli the functions under which we count lattice points and the weights are much more complicated, requiring tens of thousands of exact sum evaluations and taking quite a long time.

Summary

We proved a seventy year old conjecture  using a variety of tricks from ODEs, special functions and number theory together with computer-assisted algorithms (some of which are much more complicated than those shown above) and effectively using Mathematica’s numerical and analytic capabilities

Previously I have used Mathematica in a variety of other problems from

Riemannian geometry

spectral geometry

pure and applied PDEs, including systems such as elasticity equations

waveguide analysis and sound propagation

finite elements

programmable typesetting

...

Mathematica notebooks and printouts for Pólya’s conjecture

https://michaellevitin.net/polya.html

https://michaellevitin.net/bessels.html