# 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