Il affirme l'équivalence des deux points suivants, pour deux nombres réels et strictement positifs :
Les nombres et sont irrationnels et vérifient
Les deux suites d'entiers et , dites « suites de Beatty », forment une partition de l'ensemble ℕ*[1].
Démonstration
On suppose que les suites P et Q forment une partition de ℕ*.
Les ensembles où est un réel positif ont comme densité asymptotique. Les supports des suites P et Q forment une partition de ℕ*, donc la somme de leurs densités vaut 1 :
.
De plus, p et q ne peuvent être tous les deux rationnels, car si c'est le cas , alors . Or les suites P et Q n'ont aucun élément en commun. L'un des deux est irrationnel, et par suite les deux sont irrationnels (car )
Réciproquement, supposons que p et q sont irrationnels et . Fixons un entier k ≥ 1 et notons n (resp. m) le nombre de termes de la suite P (resp. Q) qui sont inférieurs ou égaux à k. Alors,
et .
Par définition de la partie entière et par irrationalité de p et q, nous avons les inégalités suivantes :
et
donc , autrement dit
.
De même, les nombres n' et m' de termes de P et Q qui sont inférieurs ou égaux à k – 1 vérifient :
.
Par conséquent, le nombre de termes de P égaux à k plus le nombre de termes de Q égaux à k vaut :
,
c'est-à-dire que l'entier k appartient bien à une et une seule des deux suites.
Ce résultat ne se généralise pas : il est impossible de partitionner ℕ* avec trois suites ou plus de cette forme[2]. Une question plus générale est la conjecture de Fraenkel[3].
Exemple
L'un des premiers exemples connus a été découvert dès 1907 par le mathématicien néerlandais Wythoff, indépendamment du théorème de Beatty. Pour le nombre d'or, nous avons :
Les deux suites obtenues sont alors :
, n > 0 : 1, 3, 4, 6, 8, 9, 11, 12, 14, 16, 17, 19, 21, 22, 24, 25, 27, 29, ... suite A000201 de l'OEIS
, n > 0 : 2, 5, 7, 10, 13, 15, 18, 20, 23, 26, 28, 31, 34, 36, 39, 41, 44, 47, ... suite A001950 de l'OEIS
Les couples apparaissent dans la résolution du jeu de Wythoff et caractérisent les positions à partir desquelles le joueur qui n'a pas le trait peut forcer sa victoire.