Prove2Me

Freiman lower construction: run endpoint limits

Proved
Freiman.lower_run_endpoint_limits

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

freimanlower-construction

Both actual endpoint sequences converge to the same completion with two period-3 tails, connected to the existing sSup-defined cfValue.

Preamble
import Definitions.Def_Freiman_lowerCertificates
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push

open Freiman
Formal statement
theorem Freiman.lower_run_endpoint_limits (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hr : lowerRunOffered p) :
    Filter.Tendsto (fun k : ℕ => lowerEndpoint (lowerRunPair p (k+1)) false) Filter.atTop (nhds (lowerRunValue p)) ∧
    Filter.Tendsto (fun k : ℕ => lowerEndpoint (lowerRunPair p (k+1)) true) Filter.atTop (nhds (lowerRunValue p)) := by
  sorry
Source
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), parts/j_family.tex, uniform repeated3 limit

View graph