Factorials in p-adic fields

The integers n! converge to zero at every finite place, although none is zero. This provides one sequence of rational parameters that simultaneously contracts every local unipotent one-parameter subgroup. Divisibility by each fixed prime power suffices for the convergence.

Main results

• TauCeti.tendsto_padic_natCast_factorial: the factorials tend to zero in ℚ_[p].
• TauCeti.padicValNat_factorial_eq_add_sum: Legendre's formula truncated at level h, v_p(n!) = v_p(⌊n / pʰ⌋!) + ∑_{k = 1}^{h} ⌊n / pᵏ⌋.
• TauCeti.sub_one_mul_padicValNat_factorial_pow: Legendre's formula for (pᵏ)!, (p - 1) v_p((pᵏ)!) = pᵏ - 1.
• TauCeti.norm_factorial_eq_norm_factorial_div_mul_pow, TauCeti.factorial_dvd_factorial_div_mul_pow: its consequence that n! has the norm of, and divides, ⌊n / pʰ⌋! p ^ (∑_{k = 1}^{h} ⌊n / pᵏ⌋) in ℤ_[p].
• Padic.norm_factorial_mul: ‖(p k)!‖ = p ^ (-k) ‖k!‖ in ℚ_[p], by Legendre's formula.
• Padic.rpow_neg_div_le_norm_factorial: p ^ (-n / (p - 1)) ≤ ‖n!‖ in ℚ_[p].

theorem TauCeti.tendsto_padic_natCast_factorial (p : ℕ) [hp : Fact (Nat.Prime p)] : Filter.Tendsto (fun (n : ℕ) => ↑n.factorial) Filter.atTop (nhds 0)

The factorials, viewed in a fixed p-adic field, tend to zero.

theorem TauCeti.padicValNat_factorial_eq_add_sum (p : ℕ) [Fact (Nat.Prime p)] (n h : ℕ) : padicValNat p n.factorial = padicValNat p (n / p ^ h).factorial + ∑ k ∈ Finset.range h, n / p ^ (k + 1)

Legendre's formula, truncated at level h. The p-adic valuation of n! exceeds that of ⌊n / pʰ⌋! by ∑_{k = 1}^{h} ⌊n / pᵏ⌋.

theorem TauCeti.sub_one_mul_padicValNat_factorial_pow (p : ℕ) [hp : Fact (Nat.Prime p)] (k : ℕ) : (p - 1) * padicValNat p (p ^ k).factorial = p ^ k - 1

Legendre's formula for (pᵏ)!. Since pᵏ has base-p digit sum one, (p - 1) v_p((pᵏ)!) = pᵏ - 1.

theorem TauCeti.norm_factorial_eq_norm_factorial_div_mul_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (h n : ℕ) : ‖↑n.factorial‖ = ‖↑(n / p ^ h).factorial‖ * ‖↑p‖ ^ ∑ k ∈ Finset.range h, n / p ^ (k + 1)

In ℤ_p, n! has the norm of ⌊n / pʰ⌋! p ^ (∑_{k = 1}^{h} ⌊n / pᵏ⌋): by Legendre's formula both have valuation v_p(n!).

theorem TauCeti.factorial_dvd_factorial_div_mul_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (h n : ℕ) : ↑n.factorial ∣ ↑(n / p ^ h).factorial * ↑p ^ ∑ k ∈ Finset.range h, n / p ^ (k + 1)

In ℤ_p, n! divides ⌊n / pʰ⌋! p ^ (∑_{k = 1}^{h} ⌊n / pᵏ⌋): by Legendre's formula both have valuation v_p(n!).

theorem Padic.rpow_neg_div_le_norm_factorial {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) : ↑p ^ (-(↑n / (↑p - 1))) ≤ ‖↑n.factorial‖

The norm of n! in ℚ_[p] is bounded below by p ^ (-n / (p - 1)), by Legendre's formula. This gives the factorial denominator bound for the p-adic exponential.

theorem Padic.norm_factorial_mul {p : ℕ} [Fact (Nat.Prime p)] (k : ℕ) : ‖↑(p * k).factorial‖ = ↑p ^ (-↑k) * ‖↑k.factorial‖

The factorial of p k has p-adic norm p ^ (-k) ‖k!‖: by Legendre's formula, passing from k! to (p k)! raises the valuation by k.