Local Perron values are continuous under coordinatewise convergence of words

Proved

Freiman.localValue_coordinate_limit

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

continued-fractionslagrange-spectrummarkov-spectrumnumber-theory

If every coordinate in a sequence of positive digit words eventually agrees with a limiting word, then every fixed local Perron value converges to the corresponding local value of the limiting word. No global alphabet bound is required for this continuity statement.

Preamble

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

Formal statement

namespace Freiman

theorem localValue_coordinate_limit (A : ℕ → ℤ → ℕ+) (b : ℤ → ℕ+)
    (h : ∀ i : ℤ, ∀ᶠ n in Filter.atTop, A n i = b i) :
    ∀ i : ℤ, Filter.Tendsto (fun n => localValue (A n) i)
      Filter.atTop (nhds (localValue b i)) := by
  sorry

end Freiman

Source

Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, §1.1, immediately after equation (1.3), printed p. 7.

View graph