English
If f: N → α is eventually bounded in absolute value by a and is eventually nonincreasing, then f is CauSeq abs.
Русский
Если последовательность f стабильно ограничена по модулю и убывающая, то она является CauSeq abs.
LaTeX
$$$IsCauSeq(abs, f)$ under hypotheses of boundedness and decreasing behavior$$
Lean4
theorem of_decreasing_bounded (f : ℕ → α) {a : α} {m : ℕ} (ham : ∀ n ≥ m, |f n| ≤ a) (hnm : ∀ n ≥ m, f n.succ ≤ f n) :
IsCauSeq abs f := fun ε ε0 ↦ by
classical
let ⟨k, hk⟩ := Archimedean.arch a ε0
have h : ∃ l, ∀ n ≥ m, a - l • ε < f n :=
⟨k + k + 1, fun n hnm ↦
lt_of_lt_of_le
(show a - (k + (k + 1)) • ε < -|f n| from
lt_neg.1 <|
(ham n hnm).trans_lt
(by
rw [neg_sub, lt_sub_iff_add_lt, add_nsmul, add_nsmul, one_nsmul]
exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))))
(neg_le.2 <| abs_neg (f n) ▸ le_abs_self _)⟩
let l := Nat.find h
have hl : ∀ n : ℕ, n ≥ m → f n > a - l • ε := Nat.find_spec h
have hl0 : l ≠ 0 := fun hl0 ↦
not_lt_of_ge (ham m le_rfl)
(lt_of_lt_of_le (by have := hl m (le_refl m); simpa [hl0] using this) (le_abs_self (f m)))
obtain ⟨i, hi⟩ := not_forall.1 (Nat.find_min h (Nat.pred_lt hl0))
rw [Classical.not_imp, not_lt] at hi
exists i
intro j hj
have hfij : f j ≤ f i := (Nat.rel_of_forall_rel_succ_of_le_of_le (· ≥ ·) hnm hi.1 hj).le
rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add']
calc
f i ≤ a - Nat.pred l • ε := hi.2
_ = a - l • ε + ε := by
conv =>
rhs
rw [← Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hl0), succ_nsmul, sub_add, add_sub_cancel_right]
_ < f j + ε := add_lt_add_right (hl j (le_trans hi.1 hj)) _
