The gap n - v_p(n) grows

The p-adic valuation (and, more crudely, Nat.log p) grows slower than the identity, so n - v_p(n) → ∞. This is the coefficient-decay estimate behind convergence of the formal logarithm on (pO)^n.

theorem Nat.log_succ_le (b n : ℕ) : log b (n + 1) ≤ log b n + 1

Nat.log increases by at most one when its argument does.

theorem tendsto_sub_log_atTop {p : ℕ} (hp : 1 < p) : Filter.Tendsto (fun (n : ℕ) => n - Nat.log p n) Filter.atTop Filter.atTop

n - Nat.log p n → ∞: the base-p logarithm is sublinear.

theorem tendsto_sub_padicValNat_atTop {p : ℕ} (hp : 1 < p) : Filter.Tendsto (fun (n : ℕ) => n - padicValNat p n) Filter.atTop Filter.atTop

n - v_p(n) → ∞: the p-adic valuation is sublinear.