Inverses of natural numbers in a normed field of characteristic zero

In a normed field K of characteristic zero the norm restricts to an absolute value on ℚ. By Ostrowski's theorem it is trivial, a power of the real absolute value, or a power |·|_p ^ s of a p-adic absolute value. In each case the inverse of a positive integer has at most polynomial size: ‖n⁻¹‖ ≤ n ^ c for a constant c ≥ 0. In the p-adic case c = s (|n|_p ≥ 1 / n), in the other two cases c = 0.

Consequently ‖n⁻¹‖ qⁿ → 0 for every 0 ≤ q < 1. This is the estimate that makes termwise integration of power series lose only an arbitrarily small amount of convergence radius in characteristic zero.

Main results

• NormedField.exists_norm_inv_natCast_le_rpow: ‖(n : K)⁻¹‖ ≤ n ^ c for some c ≥ 0.
• NormedField.tendsto_norm_inv_natCast_mul_pow: ‖(n : K)⁻¹‖ * q ^ n → 0 for 0 ≤ q < 1.

theorem NormedField.exists_norm_inv_natCast_le_rpow (K : Type u_1) [NormedField K] [CharZero K] : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (n : ℕ), ‖(↑n)⁻¹‖ ≤ ↑n ^ c

Inverses of natural numbers have polynomial size. In a normed field of characteristic zero there is c ≥ 0 with ‖(n : K)⁻¹‖ ≤ n ^ c for every natural number n.

theorem NormedField.tendsto_norm_inv_natCast_mul_pow (K : Type u_1) [NormedField K] [CharZero K] {q : ℝ} (hq₀ : 0 ≤ q) (hq₁ : q < 1) : Filter.Tendsto (fun (n : ℕ) => ‖(↑n)⁻¹‖ * q ^ n) Filter.atTop (nhds 0)

In a normed field of characteristic zero, ‖(n : K)⁻¹‖ * q ^ n → 0 for every 0 ≤ q < 1: the inverses of the natural numbers grow more slowly than any exponential.