English
For a nonzero PadicSeq f, there exists N such that for all m,n ≥ N the p-adic norms |f(n)|_p and |f(m)|_p are equal.
Русский
Для ненулевой PadicSeq существует N, после которого для любых m,n ≥ N имеют место |f(n)|_p = |f(m)|_p.
LaTeX
$$∀ f ∈ CauSeq ℚ(|·|_p), (f ≠ 0) ⇒ ∃ N ∈ ℕ, ∀ m,n ≥ N, |f(n)|_p = |f(m)|_p$$
Lean4
/-- The `p`-adic norm of the entries of a nonzero Cauchy sequence of rationals is eventually
constant. -/
theorem stationary {f : CauSeq ℚ (padicNorm p)} (hf : ¬f ≈ 0) :
∃ N, ∀ m n, N ≤ m → N ≤ n → padicNorm p (f n) = padicNorm p (f m) :=
have : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (f j) :=
CauSeq.abv_pos_of_not_limZero <| not_limZero_of_not_congr_zero hf
let ⟨ε, hε, N1, hN1⟩ := this
let ⟨N2, hN2⟩ := CauSeq.cauchy₂ f hε
⟨max N1 N2, fun n m hn hm ↦
by
have : padicNorm p (f n - f m) < ε := hN2 _ (max_le_iff.1 hn).2 _ (max_le_iff.1 hm).2
have : padicNorm p (f n - f m) < padicNorm p (f n) := lt_of_lt_of_le this <| hN1 _ (max_le_iff.1 hn).1
have : padicNorm p (f n - f m) < max (padicNorm p (f n)) (padicNorm p (f m)) := lt_max_iff.2 (Or.inl this)
by_contra hne
rw [← padicNorm.neg (f m)] at hne
have hnam := add_eq_max_of_ne hne
rw [padicNorm.neg, max_comm] at hnam
rw [← hnam, sub_eq_add_neg, add_comm] at this
apply _root_.lt_irrefl _ this⟩
