beattySeq_symmDiff_beattySeq'_pos
theorem beattySeq_symmDiff_beattySeq'_pos :
∀ {r s : ℝ},
r.IsConjExponent s → symmDiff {x | ∃ k > 0, beattySeq r k = x} {x | ∃ k > 0, beattySeq' s k = x} = {n | 0 < n}
This theorem is a generalization of Rayleigh's theorem on Beatty sequences. It states that for any two real numbers `r` and `s` satisfying `1/r + 1/s = 1` and `r > 1`, the sequences `B⁺_r` and `B⁺'_s` partition the set of positive integers. Here, `B⁺_r` represents the Beatty sequence for `r` (i.e., the sequence defined by the `k`th term being the floor of `k*r`), and `B⁺'_s` represents a variant of the Beatty sequence for `s` (the sequence defined by the `k`th term being the ceiling of `k*s` minus 1). The term "partition" in this context means that every positive integer belongs to exactly one of the two sequences, and no integer appears in both sequences. This partition is equivalent to taking the symmetric difference (denoted by `symmDiff`) of the sets of integers produced by the two sequences.
More concisely: For real numbers `r > 1` and `s` such that `1/r + 1/s = 1`, the Beatty sequences `B⁺_r` and `B⁺'_s` defined by `k ↦ ⌊kr⌋` and `k ↦ ⌈ks - 1⌉` respectively, form a partition of the positive integers with no common elements.
|
Irrational.beattySeq'_pos_eq
theorem Irrational.beattySeq'_pos_eq :
∀ {r : ℝ}, Irrational r → {x | ∃ k > 0, beattySeq' r k = x} = {x | ∃ k > 0, beattySeq r k = x}
The theorem states that for an irrational number `r`, the sets of elements generated by two different variations of the Beatty sequence, `B⁺_r` and `B⁺'_r`, are the same. Specifically, the set of integers that can be obtained by taking any positive integer `k` and evaluating `B⁺'_r` at `k` (i.e., `⌈k * r⌉ - 1`) is equal to the set of integers that can be obtained by evaluating `B⁺_r` at `k` (i.e., `⌊k * r⌋`).
More concisely: For any irrational number `r`, the sets generated by the Beatty sequences `B⁺_r` and `B⁺'_r` are equal, i.e., {⌊k * r⌋ | k ∈ ℕ} = {⌈k * r⌉ - 1 | k ∈ ℕ}.
|
Irrational.beattySeq_symmDiff_beattySeq_pos
theorem Irrational.beattySeq_symmDiff_beattySeq_pos :
∀ {r s : ℝ},
r.IsConjExponent s →
Irrational r → symmDiff {x | ∃ k > 0, beattySeq r k = x} {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}
**Rayleigh's Theorem** about Beatty sequences states that if `r` is an irrational number greater than 1, and `1/r + 1/s = 1`, then the Beatty sequences generated by `r` and `s` partition the positive integers. In other words, the symmetric difference of the set of positive integers produced by the Beatty sequence for `r` and the set of positive integers produced by the Beatty sequence for `s` equals the set of all positive integers. The Beatty sequence for a real number `r` is defined such that the `k`th term is the greatest integer less than or equal to `k * r`.
More concisely: If `r` and `s` are irrational numbers greater than 1 satisfying `1/r + 1/s = 1`, then the Beatty sequences generated by `r` and `s` have a symmetric difference equal to the set of all positive integers.
|
compl_beattySeq
theorem compl_beattySeq :
∀ {r s : ℝ}, r.IsConjExponent s → {x | ∃ k, beattySeq r k = x}ᶜ = {x | ∃ k, beattySeq' s k = x}
This theorem is a generalization of Rayleigh's theorem on Beatty sequences. It states that for any real numbers `r` and `s` where `r` is greater than 1, and the sum of their reciprocals equals 1 (i.e., `1/r + 1/s = 1`), the set complement of the Beatty sequence for `r` is equal to the variant Beatty sequence for `s`. In other words, every integer that is not in the Beatty sequence for `r` (`B_r`) is in the variant Beatty sequence for `s` (`B'_s`), and vice versa. The Beatty sequence for a real number `r` is defined as the sequence of integer parts of the multiples of `r`, and the variant Beatty sequence for `r` is defined as the sequence of ceiling parts of the multiples of `r` minus 1.
More concisely: For real numbers `r` and `s` with `r > 1` and `1/r + 1/s = 1`, the set complement of the Beatty sequence of `r` equals the variant Beatty sequence of `s`.
|