A convergent subsequence of words centred farther and farther right

Proved

Freiman.shifted_words_subsequence

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

continued-fractionslagrange-spectrummarkov-spectrumnumber-theory

Words shifted to strictly increasing nonnegative centres have a coordinatewise eventually constant subsequence whenever the original right tail has a finite digit bound. The limit is a two-sided word with the same bound.

Preamble

import Definitions.Def_Freiman_symbolicMarkovSpectrum
import Mathlib.Topology.Instances.Real.Lemmas

Formal statement

namespace Freiman

theorem shifted_words_subsequence (a : ℤ → ℕ+) (M N : ℕ)
    (hbound : ∀ n : ℕ, N ≤ n → (a (n : ℤ) : ℕ) ≤ M)
    (u : ℕ → ℕ) (hu : StrictMono u) :
    ∃ v : ℕ → ℕ, StrictMono v ∧
      ∃ b : ℤ → ℕ+,
        (∀ i : ℤ, (b i : ℕ) ≤ M) ∧
        (∀ i : ℤ, ∀ᶠ n in Filter.atTop,
          a ((u (v n) : ℤ) + i) = b i) := by
  sorry

end Freiman

Source

Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, §1.2, Theorem 1.3, diagonal-subsequence argument, printed p. 8.

View graph