English
If a sequence f: ℕ → ℤ satisfies p^i ∣ f(i+1) − f(i) for all i, then the sequence (f(i)) considered in the p-adic norm is a Cauchy sequence.
Русский
Если последовательность f(n) с p-adic нормой удовлетворяет p^i ∣ f(i+1) − f(i) для всех i, то она является последовательностью Коши по p-адической норме.
LaTeX
$$$IsCauSeq\\ (padicNorm\\ p)\\ (f \\cdot)$$$
Lean4
theorem isCauSeq_padicNorm_of_pow_dvd_sub (f : ℕ → ℤ) (p : ℕ) [Fact p.Prime] (hi : ∀ i, (p : ℤ) ^ i ∣ f (i + 1) - f i) :
IsCauSeq (padicNorm p) (f ·) := by
intro ε hε
obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt_rat p hε
simp only [← Int.cast_sub]
refine ⟨k, fun i hik ↦ (padicNorm.dvd_iff_norm_le.mp ?_).trans_lt hk⟩
obtain ⟨i, rfl⟩ := exists_add_of_le hik
clear hik
induction i with
| zero => simp
| succ n IH =>
have : (↑(p ^ k) : ℤ) ∣ ↑p ^ (k + n) := ⟨p ^ n, by simp [pow_add]⟩
simpa using (this.trans (hi _)).add IH
