A symbolic Lagrange value is attained as a centred symbolic Markov value

Proved

Freiman.attain_limsup_by_shift

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

continued-fractionslagrange-spectrummarkov-spectrumnumber-theory

Every finite limsup of positive-index local values of a two-sided word can be realized as the local value at zero of another two-sided positive digit word, with all local values of the new word bounded above by that limsup.

Preamble

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

Formal statement

namespace Freiman

theorem attain_limsup_by_shift (a : ℤ → ℕ+) (t : ℝ)
    (h : HasFiniteLimsup (fun n : ℕ => localValue a (n : ℤ)) t) :
    ∃ b : ℤ → ℕ+, localValue b 0 = t ∧
      ∀ i : ℤ, localValue b i ≤ t := by
  sorry

end Freiman

Source

Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, §1.2, Theorem 1.3, final paragraph, printed p. 8.

View graph