Beatty sequences

DefinitionBeatty term#✓fully proved

For a positive integer \(n\) and a real number \(\alpha\), the Beatty term \(b_n(\alpha)\) is the natural number \(\max(\lfloor n/\alpha \rfloor, 0)\): the \(n\)-th term \(\lfloor n \cdot (1/\alpha) \rfloor\) of the Beatty sequence of slope \(1/\alpha\), truncated at \(0\). Division by zero is read as \(0\), so \(b_n(0) = 0\).

public noncomputable def beattyTerm (n : { n : ℕ // 0 < n }) (α : ℝ) : ℕ :=
  (beattySeq (1 / α) (n.val : ℤ)).toNat
Used by 3
Used byBeatty term as a natural-number floor · Beatty sequences are almost Beatty · Almost Beatty sequence

TheoremBeatty term as a natural-number floor#✓fully proved

For every positive integer \(n\) and every real number \(\alpha\), the Beatty term \(b_n(\alpha)\) equals the natural-number floor of \(n/\alpha\): the largest natural number \(m\) with \(m \le n/\alpha\) when \(n/\alpha \ge 0\), and \(0\) when \(n/\alpha < 0\). Division by zero is read as \(0\), so \(n/0 = 0\).

public theorem beattyTerm_eq_floor (n : { n : ℕ // 0 < n }) (α : ℝ) :
    beattyTerm n α = Nat.floor ((n.val : ℝ) / α)
Uses 1 · Used by 1
Statement usesBeatty term
Used byBeatty sequences are almost Beatty

DefinitionAlmost Beatty sequence#✓fully proved

Let \(\alpha\) be a real number. A sequence \((s_n)_{n \ge 1}\) of natural numbers indexed by the positive integers is an almost Beatty sequence for \(\alpha\) when \(0 < \alpha < 1\), the sequence is strictly increasing, \(s_n > 0\) for every \(n \ge 1\), and there is a natural number \(B\) with \(|s_n - b_n(\alpha)| \le B\) for every \(n \ge 1\), where \(b_n(\alpha)\) is the Beatty term, equal to \(\lfloor n/\alpha \rfloor\) once \(\alpha > 0\).

public def IsAlmostBeattySequence (s : { n : ℕ // 0 < n } → ℕ) (α : ℝ) : Prop :=
  0 < α ∧ α < 1 ∧ StrictMono s ∧
    (∀ n, 0 < s n) ∧
      ∃ B : ℕ, ∀ n, ((s n : ℤ) - (beattyTerm n α : ℤ)).natAbs ≤ B
Uses 1 · Used by 2
Statement usesBeatty term
Used byBeatty sequences are almost Beatty · Almost Beatty partition

DefinitionThree-way partition of the positive integers#✓fully proved

Three sequences \(s_1, s_2, s_3\) of natural numbers indexed by the positive integers partition the positive integers when their ranges are pairwise disjoint, that is, \(s_i(m) \ne s_j(n)\) for all \(i \ne j\) and all positive integers \(m\) and \(n\), and the union of their ranges is exactly the set of positive integers: a natural number \(k\) is a value of some \(s_i\) if and only if \(k > 0\).

public def IsPositiveNatThreeWayPartition (s1 s2 s3 : { n : ℕ // 0 < n } → ℕ) : Prop :=
  (∀ m n, s1 m ≠ s2 n) ∧
    (∀ m n, s1 m ≠ s3 n) ∧
      (∀ m n, s2 m ≠ s3 n) ∧
        ∀ k : ℕ, (∃ n, s1 n = k ∨ s2 n = k ∨ s3 n = k) ↔ 0 < k
Used by 1
Used byAlmost Beatty partition

DefinitionAlmost Beatty partition#✓fully proved

Given real numbers \(\alpha_1, \alpha_2, \alpha_3\), three sequences \(s_1, s_2, s_3\) of natural numbers indexed by the positive integers form an almost Beatty partition when, for each \(i\), the sequence \(s_i\) is an almost Beatty sequence for \(\alpha_i\), and the three sequences form a three-way partition of the positive integers: their ranges are pairwise disjoint and their union is the set of positive integers.

public def IsAlmostBeattyPartition (s1 s2 s3 : { n : ℕ // 0 < n } → ℕ) (α1 α2 α3 : ℝ) : Prop :=
  IsAlmostBeattySequence s1 α1 ∧
    IsAlmostBeattySequence s2 α2 ∧
      IsAlmostBeattySequence s3 α3 ∧ IsPositiveNatThreeWayPartition s1 s2 s3
Uses 2
Statement usesAlmost Beatty sequence · Three-way partition of the positive integers

TheoremBeatty sequences are almost Beatty#✓fully proved

For every real number \(\alpha\) with \(0 < \alpha < 1\), the sequence of Beatty terms \(n \mapsto b_n(\alpha) = \lfloor n/\alpha \rfloor\), indexed by the positive integers \(n\), is an almost Beatty sequence for \(\alpha\).

The proof takes the bound \(B = 0\) and derives strict monotonicity and positivity from \(0 < \alpha < 1\).

public theorem beattyTerm_isAlmostBeattySequence (α : ℝ) (hα0 : 0 < α) (hα1 : α < 1) :
    IsAlmostBeattySequence (fun n => beattyTerm n α) α
Uses 3
Statement usesAlmost Beatty sequence · Beatty term
Proof usesBeatty term as a natural-number floor

TheoremUspensky's theorem on Beatty partitions#✓fully proved

For a real number \(\alpha\) with \(0 < \alpha < 1\), let \(B_\alpha = \{\lfloor n/\alpha \rfloor : n \text{ an integer}, n \ge 1\}\) be its Beatty sequence. Let \(k \ge 3\) and let \(\alpha_1, \dots, \alpha_k\) be real numbers with \(0 < \alpha_i < 1\) for every \(i\). Then \(B_{\alpha_1}, \dots, B_{\alpha_k}\) do not partition the positive integers: it is not the case both that \(B_{\alpha_i} \cap B_{\alpha_j} = \emptyset\) for all \(i \ne j\) and that \(B_{\alpha_1} \cup \dots \cup B_{\alpha_k} = \{1, 2, 3, \dots\}\).

No irrationality hypothesis is imposed on the \(\alpha_i\).

theorem uspensky_no_partition_into_three_or_more_beatty_sequences
    (k : ℕ) (hk : 3 ≤ k) (α : Fin k → ℝ)
    (hαpos : ∀ i, 0 < α i) (hαlt : ∀ i, α i < 1) :
    ¬ ((Set.univ : Set (Fin k)).PairwiseDisjoint
        (fun i => {x : ℤ | ∃ n : ℤ, 0 < n ∧ beattySeq (1 / α i) n = x}) ∧
      (⋃ i, {x : ℤ | ∃ n : ℤ, 0 < n ∧ beattySeq (1 / α i) n = x}) =
        {x : ℤ | 0 < x})
Sources

TheoremBeatty's theorem and its converse#●ready to prove

Let \(\alpha\) and \(\beta\) be positive real numbers. The set of the numbers \(\lfloor k\alpha\rfloor\) for positive integers \(k\) and the set of the numbers \(\lfloor k\beta\rfloor\) for positive integers \(k\) are disjoint and their union is the set of positive integers if and only if \(\alpha\) is irrational and \(\alpha^{-1} + \beta^{-1} = 1\).

The hypothesis \(\beta > 0\) cannot be dropped: for irrational \(0 < \alpha < 1\) the number \(\beta\) with \(\alpha^{-1} + \beta^{-1} = 1\) is negative, and the two sets do not partition the positive integers.

public theorem_wanted beatty_complementary_iff_irrational_inv_add_inv {α β : ℝ}
    (hα : 0 < α) (hβ : 0 < β) :
    (Disjoint {beattySeq α k | k > 0} {beattySeq β k | k > 0} ∧
        {beattySeq α k | k > 0} ∪ {beattySeq β k | k > 0} = {n : ℤ | 0 < n}) ↔
      (Irrational α ∧ α⁻¹ + β⁻¹ = 1)
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Theorem 1 (Beatty–Rayleigh).

TheoremCounting \(\beta\)-Beatty terms between \(\lfloor n\alpha\rfloor\) and \(\lfloor n\beta\rfloor\)#●ready to prove

Let \(\alpha\) be an irrational number with \(1 < \alpha < 2\), let \(\beta\) be a real number with \(\alpha^{-1} + \beta^{-1} = 1\), and let \(B\) be the set of the numbers \(\lfloor k\beta\rfloor\) for positive integers \(k\). Then for every positive integer \(n\), the number of elements of \(B\) in the open interval \((\lfloor n\alpha\rfloor, \lfloor n\beta\rfloor)\) equals \(\lfloor n(2 - \alpha)\rfloor\).

By Beatty's theorem, the Beatty sequences of \(\alpha\) and \(\beta\) are then complementary.

public theorem_wanted beatty_card_compl_between_eq_floor {α β : ℝ} (hirr : Irrational α)
    (hα1 : 1 < α) (hα2 : α < 2) (hαβ : α⁻¹ + β⁻¹ = 1) {n : ℤ} (hn : 0 < n) :
    ((Ioo (beattySeq α n) (beattySeq β n) ∩ {beattySeq β k | k > 0}).ncard : ℤ) =
      beattySeq (2 - α) n
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Theorem 3.

TheoremCounting \(\alpha\)-Beatty terms between \(\lfloor n\alpha\rfloor\) and \(\lfloor n\beta\rfloor\)#●ready to prove

Let \(\alpha\) be an irrational number with \(1 < \alpha < 2\), let \(\beta\) be a real number with \(\alpha^{-1} + \beta^{-1} = 1\), and let \(A\) be the set of the numbers \(\lfloor k\alpha\rfloor\) for positive integers \(k\). Then for every positive integer \(n\), the number of elements of \(A\) in the open interval \((\lfloor n\alpha\rfloor, \lfloor n\beta\rfloor)\) equals \(\lfloor n(\beta - 2)\rfloor\).

By Beatty's theorem, the Beatty sequences of \(\alpha\) and \(\beta\) are then complementary.

public theorem_wanted beatty_card_self_between_eq_floor {α β : ℝ} (hirr : Irrational α)
    (hα1 : 1 < α) (hα2 : α < 2) (hαβ : α⁻¹ + β⁻¹ = 1) {n : ℤ} (hn : 0 < n) :
    ((Ioo (beattySeq α n) (beattySeq β n) ∩ {beattySeq α k | k > 0}).ncard : ℤ) =
      beattySeq (β - 2) n
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Theorem 4.

TheoremPolanco's floor identity for \(\lfloor (2 - \alpha) n \rfloor\)#●ready to prove

Let \(\alpha\) be an irrational real number with \(1 < \alpha < 2\), let \(\beta\) be a real number with \(\alpha^{-1} + \beta^{-1} = 1\), and write \(a_m = \lfloor m\alpha \rfloor\) and \(b_m = \lfloor m\beta \rfloor\) for integers \(m\) (so \(b_0 = 0\)). Then for every positive integer \(n\),

\[ \lfloor \beta^{-1} (b_{n-1} + 1) \rfloor - \lfloor \beta^{-1} a_n \rfloor = \lfloor (2 - \alpha) n \rfloor. \]

Since \(\alpha > 1\), Beatty's theorem says that the conditions "\(\alpha\) is irrational and \(\alpha^{-1} + \beta^{-1} = 1\)" mean exactly that \((a_n)_{n \ge 1}\) and \((b_n)_{n \ge 1}\) are complementary Beatty sequences.

public theorem_wanted beatty_floor_inv_sub_eq_floor_two_sub {α β : ℝ} (hirr : Irrational α)
    (hα1 : 1 < α) (hα2 : α < 2) (hαβ : α⁻¹ + β⁻¹ = 1) {n : ℤ} (hn : 0 < n) :
    ⌊β⁻¹ * ((beattySeq β (n - 1) + 1 : ℤ) : ℝ)⌋ - ⌊β⁻¹ * (beattySeq α n : ℝ)⌋ =
      beattySeq (2 - α) n
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Theorem 5, identity (7).

TheoremPolanco's floor identity for \(\lfloor (\beta - 2) n \rfloor\)#●ready to prove

Let \(\alpha\) be an irrational real number with \(1 < \alpha < 2\), let \(\beta\) be a real number with \(\alpha^{-1} + \beta^{-1} = 1\), and write \(a_n = \lfloor n\alpha \rfloor\) and \(b_n = \lfloor n\beta \rfloor\). Then for every positive integer \(n\),

\[ \lfloor \alpha^{-1} b_n \rfloor - \lfloor \alpha^{-1} (a_n + 1) \rfloor = \lfloor (\beta - 2) n \rfloor. \]

Since \(\alpha > 1\), Beatty's theorem says that the conditions "\(\alpha\) is irrational and \(\alpha^{-1} + \beta^{-1} = 1\)" mean exactly that \((a_n)_{n \ge 1}\) and \((b_n)_{n \ge 1}\) are complementary Beatty sequences.

public theorem_wanted beatty_floor_inv_sub_eq_floor_sub_two {α β : ℝ} (hirr : Irrational α)
    (hα1 : 1 < α) (hα2 : α < 2) (hαβ : α⁻¹ + β⁻¹ = 1) {n : ℤ} (hn : 0 < n) :
    ⌊α⁻¹ * (beattySeq β n : ℝ)⌋ - ⌊α⁻¹ * ((beattySeq α n + 1 : ℤ) : ℝ)⌋ =
      beattySeq (β - 2) n
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Theorem 5, identity (8).

TheoremThe \(\beta\)-Beatty counts between \(\lfloor n\alpha\rfloor\) and \(\lfloor n\beta\rfloor\) form a Beatty sequence#●ready to prove

The \(\beta\)-Beatty counts between \(\lfloor n\alpha\rfloor\) and \(\lfloor n\beta\rfloor\) form a Beatty sequence. Let \(\alpha\) be an irrational number with \(1 < \alpha < 2\), let \(\beta\) be a real number with \(\alpha^{-1} + \beta^{-1} = 1\), and let \(B\) be the set of the numbers \(\lfloor k\beta\rfloor\) for positive integers \(k\). Then there is a real number \(r\) with \(0 < r < 1\) such that for every positive integer \(n\), the number of elements of \(B\) in the open interval \((\lfloor n\alpha\rfloor, \lfloor n\beta\rfloor)\) equals \(\lfloor nr\rfloor\).

By Beatty's theorem, the Beatty sequences of \(\alpha\) and \(\beta\) are then complementary.

public theorem_wanted beatty_card_compl_between_isBeatty {α β : ℝ} (hirr : Irrational α)
    (hα1 : 1 < α) (hα2 : α < 2) (hαβ : α⁻¹ + β⁻¹ = 1) :
    ∃ r : ℝ, 0 < r ∧ r < 1 ∧ ∀ n : ℤ, 0 < n →
      ((Ioo (beattySeq α n) (beattySeq β n) ∩ {beattySeq β k | k > 0}).ncard : ℤ) =
        beattySeq r n
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Corollary 3.

TheoremMultiplicities of the values of \(\lfloor n\alpha\rfloor\) for \(1/(k + 1) < \alpha < 1/k\)#●ready to prove

Let \(k\) be a positive integer and let \(\alpha\) be a real number with \(1/(k + 1) < \alpha < 1/k\). Then every non-negative integer \(t\) equals \(\lfloor n\alpha\rfloor\) for exactly \(k\) or exactly \(k + 1\) positive integers \(n\), there are infinitely many \(t\) for which it is exactly \(k\), and there are infinitely many \(t\) for which it is exactly \(k + 1\).

public theorem_wanted beatty_floor_fiber_card_eq_or_eq_succ {α : ℝ} {k : ℕ}
    (h1 : 1 / ((k : ℝ) + 1) < α) (h2 : α < 1 / (k : ℝ)) :
    (∀ t : ℕ, {n : ℕ | 0 < n ∧ ⌊(n : ℝ) * α⌋ = t}.ncard = k ∨
        {n : ℕ | 0 < n ∧ ⌊(n : ℝ) * α⌋ = t}.ncard = k + 1) ∧
      {t : ℕ | {n : ℕ | 0 < n ∧ ⌊(n : ℝ) * α⌋ = t}.ncard = k}.Infinite ∧
      {t : ℕ | {n : ℕ | 0 < n ∧ ⌊(n : ℝ) * α⌋ = t}.ncard = k + 1}.Infinite
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Lemma 1.

TheoremMultiplicity \(k + 1\) for \(\alpha\) is multiplicity \(k\) for \(\alpha/(1 - \alpha)\)#●ready to prove

Let \(k\) be a positive integer, let \(\alpha\) be a real number with \(1/(k + 1) < \alpha < 1/k\), and let \(\beta = \alpha/(1 - \alpha)\). Then a non-negative integer \(t\) equals \(\lfloor n\alpha\rfloor\) for exactly \(k + 1\) positive integers \(n\) if and only if it equals \(\lfloor n\beta\rfloor\) for exactly \(k\) positive integers \(n\).

public theorem_wanted beatty_floor_fiber_card_succ_iff {α : ℝ} {k : ℕ}
    (h1 : 1 / ((k : ℝ) + 1) < α) (h2 : α < 1 / (k : ℝ)) (t : ℕ) :
    {n : ℕ | 0 < n ∧ ⌊(n : ℝ) * α⌋ = t}.ncard = k + 1 ↔
      {n : ℕ | 0 < n ∧ ⌊(n : ℝ) * (α / (1 - α))⌋ = t}.ncard = k
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Lemma 2.

TheoremThe values of \(\lfloor n\alpha\rfloor\) of each multiplicity form Beatty sets#●ready to prove

Let \(k\) be a positive integer and let \(\alpha\) be an irrational number with \(1/(k + 1) < \alpha < 1/k\). Then there are real numbers \(\gamma > 0\) and \(\delta > 0\) such that the positive integers \(t\) that equal \(\lfloor n\alpha\rfloor\) for exactly \(k + 1\) positive integers \(n\) are exactly the numbers \(\lfloor m\gamma\rfloor\) for positive integers \(m\), and the positive integers \(t\) that equal \(\lfloor n\alpha\rfloor\) for exactly \(k\) positive integers \(n\) are exactly the numbers \(\lfloor m\delta\rfloor\) for positive integers \(m\).

public theorem_wanted beatty_floor_fiber_card_sets_isBeatty {α : ℝ} {k : ℕ}
    (hirr : Irrational α) (h1 : 1 / ((k : ℝ) + 1) < α) (h2 : α < 1 / (k : ℝ)) :
    ∃ γ δ : ℝ, 0 < γ ∧ 0 < δ ∧
      {t : ℤ | 0 < t ∧ {n : ℕ | 0 < n ∧ ⌊(n : ℝ) * α⌋ = t}.ncard = k + 1} =
        {beattySeq γ m | m > 0} ∧
      {t : ℤ | 0 < t ∧ {n : ℕ | 0 < n ∧ ⌊(n : ℝ) * α⌋ = t}.ncard = k} =
        {beattySeq δ m | m > 0}
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Corollary 1.

TheoremMultiplicities of \(\lfloor n\alpha\rfloor\) are \(k\) plus the indicator of a Beatty set#●ready to prove

Let \(k\) be a positive integer and let \(\alpha\) be an irrational number with \(1/(k + 1) < \alpha < 1/k\). Then there is a real number \(\delta > 0\) such that, writing \(D\) for the set of the numbers \(\lfloor m\delta\rfloor\) for positive integers \(m\), every non-negative integer \(t\) equals \(\lfloor n\alpha\rfloor\) for exactly \(k + 1\) positive integers \(n\) if \(t \in D\), and for exactly \(k\) positive integers \(n\) if \(t \notin D\).

public theorem_wanted beatty_floor_fiber_card_eq_add_indicator {α : ℝ} {k : ℕ}
    (hirr : Irrational α) (h1 : 1 / ((k : ℝ) + 1) < α) (h2 : α < 1 / (k : ℝ)) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ t : ℕ, {n : ℕ | 0 < n ∧ ⌊(n : ℝ) * α⌋ = t}.ncard =
      k + {beattySeq δ m | m > 0}.indicator (1 : ℤ → ℕ) t
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Corollary 2.

TheoremIncrements of the \(\beta\)-Beatty counts between \(\lfloor n\alpha\rfloor\) and \(\lfloor n\beta\rfloor\)#●ready to prove

Increments of the \(\beta\)-Beatty counts between \(\lfloor n\alpha\rfloor\) and \(\lfloor n\beta\rfloor\). Let \(\alpha\) be an irrational number with \(1 < \alpha < 2\), let \(\beta\) be a real number with \(\alpha^{-1} + \beta^{-1} = 1\), let \(B\) be the set of the numbers \(\lfloor k\beta\rfloor\) for positive integers \(k\), and for an integer \(m\) let \(r(m)\) be the number of elements of \(B\) in the open interval \((\lfloor m\alpha\rfloor, \lfloor m\beta\rfloor)\). Then for every positive integer \(n\), the difference \(r(n + 1) - r(n)\) is \(0\) or \(1\), and it equals \(1\) if and only if \(\lfloor (n + 1)\alpha\rfloor - \lfloor n\alpha\rfloor = 1\).

By Beatty's theorem, the Beatty sequences of \(\alpha\) and \(\beta\) are then complementary.

public theorem_wanted beatty_card_compl_between_succ_sub {α β : ℝ} (hirr : Irrational α)
    (hα1 : 1 < α) (hα2 : α < 2) (hαβ : α⁻¹ + β⁻¹ = 1) {n : ℤ} (hn : 0 < n) :
    let r : ℤ → ℤ := fun m ↦
      ((Ioo (beattySeq α m) (beattySeq β m) ∩ {beattySeq β k | k > 0}).ncard : ℤ)
    (r (n + 1) - r n = 0 ∨ r (n + 1) - r n = 1) ∧
      (r (n + 1) - r n = 1 ↔ beattySeq α (n + 1) - beattySeq α n = 1)
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Lemma 4.

TheoremIncrements of the \(\alpha\)-Beatty counts between \(\lfloor n\alpha\rfloor\) and \(\lfloor n\beta\rfloor\)#●ready to prove

Increments of the \(\alpha\)-Beatty counts between \(\lfloor n\alpha\rfloor\) and \(\lfloor n\beta\rfloor\). Let \(\beta\) be an irrational number with \(\beta > 2\), let \(\alpha\) be a real number with \(\alpha^{-1} + \beta^{-1} = 1\), let \(A\) be the set of the numbers \(\lfloor k\alpha\rfloor\) for positive integers \(k\), and for an integer \(m\) let \(c(m)\) be the number of elements of \(A\) in the open interval \((\lfloor m\alpha\rfloor, \lfloor m\beta\rfloor)\). Then for every positive integer \(n\), the difference \(c(n + 1) - c(n)\) is \(\lfloor\beta\rfloor - 2\) or \(\lfloor\beta\rfloor - 1\), and it equals \(\lfloor\beta\rfloor - 2\) if and only if \(\lfloor (n + 1)\beta\rfloor - \lfloor n\beta\rfloor = \lfloor\beta\rfloor\).

By Beatty's theorem, the Beatty sequences of \(\alpha\) and \(\beta\) are then complementary.

public theorem_wanted beatty_card_self_between_succ_sub {α β : ℝ} (hirr : Irrational β)
    (hβ : 2 < β) (hαβ : α⁻¹ + β⁻¹ = 1) {n : ℤ} (hn : 0 < n) :
    let c : ℤ → ℤ := fun m ↦
      ((Ioo (beattySeq α m) (beattySeq β m) ∩ {beattySeq α k | k > 0}).ncard : ℤ)
    (c (n + 1) - c n = ⌊β⌋ - 2 ∨ c (n + 1) - c n = ⌊β⌋ - 1) ∧
      (c (n + 1) - c n = ⌊β⌋ - 2 ↔ beattySeq β (n + 1) - beattySeq β n = ⌊β⌋)
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Lemma 5.

TheoremMultiplicities of Polanco's skipping sequence#●ready to prove

Let \(k \ge 1\) be an integer, let \(\alpha\) be an irrational real number with \((2k - 1)/k < \alpha < (2k + 1)/(k + 1)\), and let \(\beta\) be a real number with \(\alpha^{-1} + \beta^{-1} = 1\). Let \(A = \{\lfloor j\alpha \rfloor : j \ge 1\}\) and, for each positive integer \(n\), let \(c_n\) be the number of elements of \(A\) strictly between \(\lfloor n\alpha \rfloor\) and \(\lfloor n\beta \rfloor\). Let \(f(x) = 2 - 1/x\), let \(f^{k-1}\) be its \((k-1)\)-fold iterate, and let \(\delta = -1 + 1/f^{k-1}(\alpha - 1)\), that is, \(\delta = -1 + 1/(2 - 1/(2 - \cdots - 1/(\alpha - 1)))\) with \(k - 1\) twos. Then for every non-negative integer \(m\), the number of positive integers \(n\) with \(c_n = m\) is \(k\) if \(m = \lfloor j\delta \rfloor\) for some integer \(j \ge 1\), and \(k - 1\) otherwise, where an infinite set is counted as having \(0\) elements.

For \(k = 1\) this gives \(\delta = 1/(\alpha - 1) - 1 = \beta - 2\), and the multiplicity is one or zero.

public theorem_wanted beatty_skipping_card_eq_add_indicator {α β : ℝ} {k : ℕ}
    (hirr : Irrational α) (hk : 1 ≤ k) (hk1 : (2 * (k : ℝ) - 1) / k < α)
    (hk2 : α < (2 * (k : ℝ) + 1) / ((k : ℝ) + 1)) (hαβ : α⁻¹ + β⁻¹ = 1) (m : ℕ) :
    {n : ℤ | 0 < n ∧
        (Ioo (beattySeq α n) (beattySeq β n) ∩ {beattySeq α j | j > 0}).ncard = m}.ncard =
      (k - 1) + {beattySeq (-1 + 1 / (fun x : ℝ ↦ 2 - 1 / x)^[k - 1] (α - 1)) j | j > 0}.indicator
        (1 : ℤ → ℕ) m
Sources
  • Geremias Polanco, Decomposition of Beatty and Complementary Sequences, INTEGERS 25 (2025), Article A104, Lemma 6.
7 fully proved13 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.