English
A monotone function f: ℕ → ℕ with an upper bound b stabilises within at most b steps: f n = f b for all n ≥ b provided a suitable stabilisation event occurs earlier.
Русский
Непрерывная монотонная функция f: ℕ → ℕ с верхней границей b стабилизируется не позже чем за b шагов: f n = f b для всех n ≥ b при удовлетворении условия стабилизации ранее.
LaTeX
$$$\\forall f:\\mathbb{N}\\to\\mathbb{N}\\,\\forall b\\,\\forall n,\\ Monotone f\\to (\\forall m, f m \\le b)\\to (\\exists m≤b, f m = f(m+1))\\to f n = f b,$$$
Lean4
/-- A monotone function `f : ℕ → ℕ` bounded by `b`, which is constant after stabilising for the
first time, stabilises in at most `b` steps. -/
theorem stabilises_of_monotone {f : ℕ → ℕ} {b n : ℕ} (hfmono : Monotone f) (hfb : ∀ m, f m ≤ b)
(hfstab : ∀ m, f m = f (m + 1) → f (m + 1) = f (m + 2)) (hbn : b ≤ n) : f n = f b :=
by
obtain ⟨m, hmb, hm⟩ : ∃ m ≤ b, f m = f (m + 1) := by
contrapose! hfb
let rec strictMono : ∀ m ≤ b + 1, m ≤ f m
| 0, _ => Nat.zero_le _
| m + 1, hmb =>
(strictMono _ <| m.le_succ.trans hmb).trans_lt <|
(hfmono m.le_succ).lt_of_ne <| hfb _ <| Nat.le_of_succ_le_succ hmb
exact ⟨b + 1, strictMono _ le_rfl⟩
replace key : ∀ k : ℕ, f (m + k) = f (m + k + 1) ∧ f (m + k) = f m := fun k =>
Nat.rec ⟨hm, rfl⟩ (fun k ih => ⟨hfstab _ ih.1, ih.1.symm.trans ih.2⟩) k
replace key : ∀ k ≥ m, f k = f m := fun k hk => (congr_arg f (Nat.add_sub_of_le hk)).symm.trans (key (k - m)).2
exact (key n (hmb.trans hbn)).trans (key b hmb).symm
