Factorial valuations in mixed-characteristic local fields

Let K be a finite extension of ℚ_[p], and write e for its absolute ramification index. The normalized valuation on K restricts to e times the normalized valuation on ℚ_[p]. Consequently the valuation in K of a natural number n is

e * padicValNat p n.

Applying Legendre's formula gives the exact valuation of n ! and the strict estimate

(p - 1) * v_K(n !) < e * n

for positive n. If a depth i satisfies (p - 1) * i > e, this implies v_K(n !) < n * i. This is the coefficient estimate used to construct the exponential on deep units: for an element of valuation at least i, the n-th term x ^ n / n ! has positive valuation, with a margin that grows linearly in n.

Main results

• TauCeti.sub_one_mul_natCastValuation_factorial: Legendre's formula after base change.
• TauCeti.sub_one_mul_natCastValuation_factorial_lt_of_ne_zero: the strict factorial estimate.
• TauCeti.natCastValuation_factorial_lt_mul_of_absoluteRamificationIndex_lt_of_ne_zero: the estimate at a depth in the exponential's convergence range.

References

• J.-P. Serre, Local Fields, Chapter II, §5.
• J. Neukirch, Algebraic Number Theory, Chapter II, §5.

theorem TauCeti.sub_one_mul_natCastValuation_factorial (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] (n : ℕ) : (p - 1) * natCastValuation K n.factorial ⋯ = absoluteRamificationIndex K p * (n - (p.digits n).sum)

Legendre's formula for the normalized valuation of a factorial in a finite extension of ℚ_[p].

theorem TauCeti.sub_one_mul_natCastValuation_factorial_lt_of_ne_zero (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] {n : ℕ} (hn : n ≠ 0) : (p - 1) * natCastValuation K n.factorial ⋯ < absoluteRamificationIndex K p * n

The normalized valuation of n ! satisfies the strict Legendre bound after base change to a finite extension of ℚ_[p].

theorem TauCeti.natCastValuation_factorial_lt_mul_of_absoluteRamificationIndex_lt_of_ne_zero (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i n : ℕ} (hi : absoluteRamificationIndex K p < (p - 1) * i) (hn : n ≠ 0) : natCastValuation K n.factorial ⋯ < n * i

At every depth i in the exponential convergence range (p - 1) * i > e, the valuation of n ! is strictly smaller than n * i for positive n.