English
Let r > 1 be irrational and let s be a real number with 1/r + 1/s = 1. Then the Beatty sequences B_r = { floor(r k) : k > 0 } and B_s = { floor(s k) : k > 0 } partition the positive integers.
Русский
Пусть r > 1 иррационально. Пусть s удовлетворяет 1/r + 1/s = 1. Тогда последовательности Бетти B_r = { ⌊rk⌋ : k > 0 } и B_s = { ⌊sk⌋ : k > 0 } разбивают множество положительных целых чисел.
LaTeX
$$$\\left\\{ \\lfloor r k \\rfloor : k>0 \\right\\} \\triangle \\left\\{ \\lfloor s k \\rfloor : k>0 \\right\\} = \\{ n \\in \\mathbb{N} : 0 < n \\}$, given $r>1$ irrational and $\\dfrac{1}{r}+\\dfrac{1}{s}=1$.$$
Lean4
/-- **Rayleigh's theorem** on Beatty sequences. Let `r` be an irrational number greater than 1, and
`1/r + 1/s = 1`. Then `B⁺_r` and `B⁺_s` partition the positive integers. -/
theorem beattySeq_symmDiff_beattySeq_pos {r s : ℝ} (hrs : r.HolderConjugate s) (hr : Irrational r) :
{beattySeq r k | k > 0} ∆ {beattySeq s k | k > 0} = {n | 0 < n} := by
rw [← hr.beattySeq'_pos_eq, beattySeq'_symmDiff_beattySeq_pos hrs]
