Wolfram Cloud Document

Pólya's conjecture for the disk: a computer-assisted proof
by Michael Levitin
(C) M. Levitin, I. Polterovich, and D. A. Sher

For simplicity, this notebook differs slightly from the one used in the actual calculations described in the paper, by removing some non-essential embellishments. As a result, the output may also be slightly different from that available for download at https://michaellevitin.net/polya.html

This script reads files smallqminus.csv, smallqplus.csv, capitalqminus.csv, capitalqplus.csv, and capitalqr.csv from https://michaellevitin.net/polya.html

Article abstract

The celebrated Pólya’s conjecture (1954) in spectral geometry states that the eigenvalue counting functions of the Dirichlet and Neumann Laplacian on a bounded Euclidean domain can be estimated from above and below, respectively, by the leading term of Weyl’s asymptotics. Pólya’s conjecture is known to be true for domains which tile the space, and, in addition, for some special domains in higher dimensions. In this paper, we prove Pólya’s conjecture for the disk, making it the first non-tiling planar domain for which the conjecture is verified. Along the way, we develop the known links between the spectral problems in the disk and certain lattice counting problems. The key novel ingredient is the observation, made in recent work of the last named author, that the corresponding eigenvalue and lattice counting functions are related not only asymptotically, but in fact satisfy certain uniform bounds. Our proofs are purely analytic for the values of the spectral parameter above some large (but explicitly given) number. Below that number we give a rigorous computer-assisted proof which converges in a finite number of steps and uses only integer arithmetic.

Notebook initialisation

SetDirectory[NotebookDirectory[]];<<MaTeX`texStyle={};SetOptions[MaTeX,"BasePreamble"{"\\usepackage{amsmath}","\\usepackage{xcolor}","\\usepackage{fourier}","\\usepackage{ebgaramond}"},FontSize11];

Coefficients of
h

and
h


Loading the coefficients of



and



and converting them into fractions (compare with Table 4 in the paper)

In[]:=

qdataminus=Import["https://michaellevitin.net/PolyaData/smallqminus.csv"];qdataplus=Import["https://michaellevitin.net/PolyaData/smallqplus.csv"];Qdataminus=Import["https://michaellevitin.net/PolyaData/capitalqminus.csv"];Qdataplus=Import["https://michaellevitin.net/PolyaData/capitalqplus.csv"];QdataR=Import["https://michaellevitin.net/PolyaData/capitalqr.csv"];

In what follows qminus, qplus, Qminus, Qplus, and QR are the indexed quantities

and

from the paper, with the second index shifted by one, so that qminus[[i]][[j]]=

-,i,j-1

, etc.

In[]:=

qminus=Table[qdataminus[[i,j]]/qdataminus[[i,j+1]],{i,14},{j,1,11,2}];qminus//TableFormqplus=Table[qdataplus[[i,j]]/qdataplus[[i,j+1]],{i,14},{j,1,11,2}];qplus//TableForm

Out[]//TableForm=

1475 5022	- 2569 5307	523 3282	9 3380	97 7232	8 6631
378 1531	- 2127 4705	1570 9753	9 1093	37 2522	18 4573
86 423	- 2084 4967	490 2981	25 1711	57 3251	31 3978
290 1779	- 626 1621	429 2525	119 5268	41 1791	33 2311
155 1229	- 1444 4109	1283 7199	119 3550	25 762	115 4272
237 2554	- 342 1087	400 2099	28 559	80 1527	417 7490
115 1636	- 794 2785	872 4277	101 1449	174 2135	219 2057
254 4491	- 649 2457	530 2457	347 3892	203 1751	272 1541
212 4829	- 1015 4197	748 3237	467 3967	604 3441	1284 4039
36 1111	- 687 3155	205 814	101 620	1529 5279	2077 3227
181 8165	- 1564 8181	777 2759	1672 6895	1412 2599	15016 9655
51 3821	- 411 2555	741 2254	961 2349	2877 2279	7097 1402
8 1293	- 431 3474	524 1251	4199 4694	18111 3989	130957 4318
7 5895	- 197 2762	3433 4793	29881 6338	164653 2318	4383291 3083

Out[]//TableForm=

1475 5022	- 1733 3580	523 3282	5 1878	97 7232	4 3317
378 1531	- 1363 3015	1570 9753	20 2429	37 2522	13 3303
86 423	- 819 1952	490 2981	43 2943	57 3251	79 10138
290 1779	- 531 1375	429 2525	63 2789	41 1791	31 2171
155 1229	- 1172 3335	1283 7199	155 4624	25 762	101 3752
237 2554	- 499 1586	400 2099	225 4492	80 1527	183 3287
115 1636	- 1192 4181	872 4277	251 3601	174 2135	275 2583
254 4491	- 705 2669	530 2457	865 9702	203 1751	275 1558
212 4829	- 1104 4565	748 3237	469 3984	604 3441	872 2743
36 1111	- 871 4000	205 814	642 3941	1529 5279	475 738
181 8165	- 2214 11581	777 2759	1898 7827	1412 2599	12680 8153
51 3821	- 351 2182	741 2254	988 2415	2877 2279	13460 2659
8 1293	- 481 3877	524 1251	14777 16519	18111 3989	326331 10760
7 5895	- 99 1388	3433 4793	11546 2449	164653 2318	7529649 5296

In[]:=

Qminus=Table[Qdataminus[[i,j]]/Qdataminus[[i,j+1]],{i,13},{j,1,11,2}];Qplus=Table[Qdataplus[[i,j]]/Qdataplus[[i,j+1]],{i,13},{j,1,11,2}];QR=Table[QdataR[[i,j]]/QdataR[[i,j+1]],{i,10},{j,1,3,2}];Qminus//TableFormQplus//TableFormQR//TableForm

Out[]//TableForm=

1097 3735	- 1733 3580	316 1983	5 1878	56 4175	0
776 3143	- 1363 3015	844 5243	20 2429	25 1704	4 1607
995 4894	- 819 1952	514 3127	43 2943	59 3365	13 2299
647 3969	- 531 1375	569 3349	63 2789	85 3713	13 1231
493 3909	- 1172 3335	977 5482	155 4624	98 2987	52 2673
76 819	- 499 1586	796 4177	225 4492	126 2405	259 6795
177 2518	- 1192 4181	1061 5204	251 3601	137 1681	306 3613
163 2882	- 705 2669	1222 5665	865 9702	430 3709	579 4261
410 9339	- 1104 4565	632 2735	469 3984	835 4757	469 2004
79 2438	- 871 4000	854 3391	642 3941	601 2075	1401 3152
73 3293	- 2214 11581	541 1921	1898 7827	615 1132	1716 1763
37 2772	- 351 2182	1267 3854	988 2415	611 484	3352 1255
18 2909	- 481 3877	1794 4283	14777 16519	7278 1603	37396 3379

Out[]//TableForm=

1097 3735	- 2569 5307	316 1983	9 3380	56 4175	10 4017
776 3143	- 2127 4705	844 5243	9 1093	25 1704	6 1061
995 4894	- 2084 4967	514 3127	25 1711	59 3365	45 4261
647 3969	- 626 1621	569 3349	119 5268	85 3713	72 3701
493 3909	- 1444 4109	977 5482	119 3550	98 2987	319 8369
76 819	- 342 1087	796 4177	28 559	126 2405	140 1653
177 2518	- 794 2785	1061 5204	101 1449	137 1681	760 5593
163 2882	- 649 2457	1222 5665	347 3892	430 3709	491 2098
410 9339	- 1015 4197	632 2735	467 3967	835 4757	1381 3107
79 2438	- 687 3155	854 3391	101 620	601 2075	1570 1613
73 3293	- 1564 8181	541 1921	1672 6895	615 1132	6493 2431
37 2772	- 411 2555	1267 3854	961 2349	611 484	48596 4391
18 2909	- 431 3474	1794 4283	4199 4694	7278 1603	1005239 8009

This section is for illustrative purposes only. We demonstrate (numerically) the validity of the inequalities above, cf. Figure 9 in the paper. We omit some embellishments made in the paper in order to improve the graphics presentation.

Counting the points and setting up the iteration processes

Example

The following auxiliary function Fori[α0, d] realises Forišek’s algorithm (see the citation in the paper) of finding the smallest possible denominator rational approximation to a rational number α0>0 within the interval (α0-d, α0+d). Its typical uses are Fori[α0+ϵ, δ] with small rational values 0<δ<ϵ to give a rational approximation of α0 from above with a small denominator, and Fori[α0-ϵ, δ] to give a rational approximation of α0 from below with a small denominator. Using Fori is not, strictly speaking, necessary, but ensures that the denominators of the fractions appearing in the iteration processes are kept relatively small, at the cost of slightly slowing the processes.

Example of the use of Fori

Example

Actual calculations

The following functions (shown here without commands used for output into external files) have been used to perform the actual calculations. The parameter freq in both functions stands for the frequency of screen output, thus taking freq=1 will output on each step, and freq=100 on every hundredth step. The parameter id is a string used to identify the output from a particular calculation (useful in parallelised processes). For ease of observation only, some output is converted into floating point numbers.

Examples

The full computer-assisted proof can be verified, for example, by executing the following command (WARNING: may take a very long time, especially on slower computers; ignore the indication of remaining time)

Article abstract

Notebook initialisation

Coefficients of h and h

Counting the points and setting up the iteration processes

Example

Example of the use of Fori

Example

Actual calculations

Examples

Coefficients of
h

and
h
