Theorems · Theorem · number theory

compl_beattySeq

• 1000+ list: Beatty's theorem

∀ {r s : ℝ}, r.HolderConjugate 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.

Defined in

Mathlib.NumberTheory.Rayleigh

Cited by

2 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound