Sublinear growth of the p-adic valuation of natural numbers

Since p ^ padicValNat p n ∣ n, the valuation padicValNat p n is at most logarithmic in n. This file records the consequence that any fixed multiple of it, shifted by any constant, is eventually below n:

∀ᶠ n in atTop, M + c * padicValNat p n ≤ n,

together with the uniform form c * padicValNat p n ≤ n + C for some constant C, and the sharp bound e * padicValNat p n < i * (n - 1) for n ≥ 2 whenever e < (p - 1) * i.

These are the estimates that make a power series with coefficients 1 / n converge on the open unit disc of a p-adic field, for instance the logarithm series, and make its nonlinear terms strictly smaller than the linear one on sufficiently deep inputs.

The logarithmic form of the bound, padicValNat p n * log p ≤ log n (so in particular padicValNat p n ≤ log n / log 2), bounds the exponents of an integer composed of finitely many primes by its logarithm, as needed for gaps between such integers and for exponential Diophantine equations.

theorem TauCeti.eventually_add_mul_padicValNat_le (p M c : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, M + c * padicValNat p n ≤ n

The p-adic valuation of natural numbers grows sublinearly: for all constants M and c, eventually M + c * padicValNat p n ≤ n.

theorem TauCeti.exists_mul_padicValNat_le_add (p c : ℕ) : ∃ (C : ℕ), ∀ (n : ℕ), c * padicValNat p n ≤ n + C

Scaled by any constant c, the p-adic valuation of natural numbers is bounded by n up to an additive constant: for some C, c * padicValNat p n ≤ n + C for all n.

theorem TauCeti.mul_padicValNat_lt_mul_sub_one {p e i n : ℕ} (hi : e < (p - 1) * i) (hn : 2 ≤ n) : e * padicValNat p n < i * (n - 1)

If e < (p - 1) * i, then e * padicValNat p n < i * (n - 1) for every n ≥ 2.

theorem TauCeti.padicValNat_mul_log_le_log (p n : ℕ) : ↑(padicValNat p n) * Real.log ↑p ≤ Real.log ↑n

The p-adic valuation of n is at most logarithmic in n: padicValNat p n * log p ≤ log n.

theorem TauCeti.padicValNat_le_log_div_log_two (p n : ℕ) : ↑(padicValNat p n) ≤ Real.log ↑n / Real.log 2

The p-adic valuation of n is at most log n / log 2.