A finite limit along shifted increasing centres is at most the right limsup

Proved

Freiman.localValue_shift_limit_le

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

continued-fractionslagrange-spectrummarkov-spectrumnumber-theory

Let the positive-index local values of a word have finite limsup t. If, at a fixed integer offset from strictly increasing nonnegative centres, the local values converge to r, then r is at most t.

Preamble

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

Formal statement

namespace Freiman

theorem localValue_shift_limit_le (a : ℤ → ℕ+) (t : ℝ)
    (h : HasFiniteLimsup (fun n : ℕ => localValue a (n : ℤ)) t)
    (s : ℕ → ℕ) (hs : StrictMono s) (i : ℤ) (r : ℝ)
    (hr : Filter.Tendsto (fun n => localValue a ((s n : ℤ) + i))
      Filter.atTop (nhds r)) :
    r ≤ t := by
  sorry

end Freiman

Source

Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, §1.2, Theorem 1.3, inequality for every fixed r in the limiting word, printed p. 8.

View graph