Rayleigh's theorem on Beatty sequences

This file proves Rayleigh's theorem on Beatty sequences. We start by proving compl_beattySeq, which is a generalization of Rayleigh's theorem, and eventually prove Irrational.beattySeq_symmDiff_beattySeq_pos, which is Rayleigh's theorem.

Main definitions

• beattySeq: In the Beatty sequence for real number r, the kth term is ⌊k * r⌋.
• beattySeq': In this variant of the Beatty sequence for r, the kth term is ⌈k * r⌉ - 1.

Main statements

Define the following Beatty sets, where r denotes a real number:

• B_r := {⌊k * r⌋ | k ∈ ℤ}
• B'_r := {⌈k * r⌉ - 1 | k ∈ ℤ}
• B⁺_r := {⌊r⌋, ⌊2r⌋, ⌊3r⌋, ...}
• B⁺'_r := {⌈r⌉-1, ⌈2r⌉-1, ⌈3r⌉-1, ...}

The main statements are:

• compl_beattySeq: Let r be a real number greater than 1, and 1/r + 1/s = 1. Then the complement of B_r is B'_s.
• beattySeq_symmDiff_beattySeq'_pos: Let r be a real number greater than 1, and 1/r + 1/s = 1. Then B⁺_r and B⁺'_s partition the positive integers.
• Irrational.beattySeq_symmDiff_beattySeq_pos: 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.

References

• Wikipedia, Beatty sequence

Tags

beatty, sequence, rayleigh, irrational, floor, positive

noncomputable def beattySeq (r : ℝ) : ℤ → ℤ

In the Beatty sequence for real number r, the kth term is ⌊k * r⌋.

Equations

• beattySeq r k = ⌊↑k * r⌋

noncomputable def beattySeq' (r : ℝ) : ℤ → ℤ

In this variant of the Beatty sequence for r, the kth term is ⌈k * r⌉ - 1.

Equations

• beattySeq' r k = ⌈↑k * r⌉ - 1

theorem compl_beattySeq {r : ℝ} {s : ℝ} (hrs : Real.IsConjugateExponent r s) : {x : ℤ | ∃ (k : ℤ), beattySeq r k = x}ᶜ = {x : ℤ | ∃ (k : ℤ), beattySeq' s k = x}

Generalization of Rayleigh's theorem on Beatty sequences. Let r be a real number greater than 1, and 1/r + 1/s = 1. Then the complement of B_r is B'_s.

theorem compl_beattySeq' {r : ℝ} {s : ℝ} (hrs : Real.IsConjugateExponent r s) : {x : ℤ | ∃ (k : ℤ), beattySeq' r k = x}ᶜ = {x : ℤ | ∃ (k : ℤ), beattySeq s k = x}

theorem beattySeq_symmDiff_beattySeq'_pos {r : ℝ} {s : ℝ} (hrs : Real.IsConjugateExponent r s) : symmDiff {x : ℤ | ∃ k > 0, beattySeq r k = x} {x : ℤ | ∃ k > 0, beattySeq' s k = x} = {n : ℤ | 0 < n}

Generalization of Rayleigh's theorem on Beatty sequences. Let r be a real 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 : Real.IsConjugateExponent r s) : symmDiff {x : ℤ | ∃ k > 0, beattySeq' r k = x} {x : ℤ | ∃ k > 0, beattySeq s k = x} = {n : ℤ | 0 < n}

theorem Irrational.beattySeq'_pos_eq {r : ℝ} (hr : Irrational r) : {x : ℤ | ∃ k > 0, beattySeq' r k = x} = {x : ℤ | ∃ k > 0, beattySeq r k = x}

Let r be an irrational number. Then B⁺_r and B⁺'_r are equal.

theorem Irrational.beattySeq_symmDiff_beattySeq_pos {r : ℝ} {s : ℝ} (hrs : Real.IsConjugateExponent r s) (hr : Irrational r) : symmDiff {x : ℤ | ∃ k > 0, beattySeq r k = x} {x : ℤ | ∃ k > 0, beattySeq s k = x} = {n : ℤ | 0 < n}

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.