# Documentation

Mathlib.NumberTheory.Rayleigh

# 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.

## 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
Instances For
noncomputable def beattySeq' (r : ) :

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

Equations
Instances For
theorem compl_beattySeq {r : } {s : } (hrs : ) :
{x : | ∃ (k : ), = x} = {x : | ∃ (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 : ) :
{x : | ∃ (k : ), = x} = {x : | ∃ (k : ), = x}
theorem beattySeq_symmDiff_beattySeq'_pos {r : } {s : } (hrs : ) :
{x : | ∃ k > 0, = x} {x : | ∃ k > 0, = 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 : ) :
{x : | ∃ k > 0, = x} {x : | ∃ k > 0, = x} = {n : | 0 < n}
theorem Irrational.beattySeq'_pos_eq {r : } (hr : ) :
{x : | ∃ k > 0, = x} = {x : | ∃ k > 0, = x}

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

theorem Irrational.beattySeq_symmDiff_beattySeq_pos {r : } {s : } (hrs : ) (hr : ) :
{x : | ∃ k > 0, = x} {x : | ∃ k > 0, = 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.