Documentation

LeanPool.GranvilleMoore.BinomPoly

The binomial polynomial at powers of p #

The rescaled binomial polynomial B_m(z) = (1/m!) ∏_{s<m} ((z-1)/(p-1) - s) of Granville's paper is engineered so that its values at the powers of p are binomial coefficients: the substitution z = p^i turns (z-1)/(p-1) into the Frobenius exponent e_i = ∑_{r<i} p^r, and the product becomes the length-m falling factorial of e_i.

This file proves that evaluation, reads it backwards as an expansion of C(e_i, m) in the powers (p^n)^i, and bounds the denominators of the coefficients β_{m,n}.

Main results #

Implementation notes #

The hypothesis for the evaluation lemmas is 2 ≤ p, not p.Prime: nothing in them is about primality, and both p = 0 and p = 1 have to be excluded because (p : ℚ) - 1 is the denominator being cleared and p ^ k - 1 the numerator. Primality enters only with the p-adic valuation.

The p-integrality of the coefficients is usually stated as the valuation inequality v_p(β_{m,n}) ≥ -v_p(m!), and that is what is proved here, in Mathlib's padicValRat. It is however derived from a sharper and purely algebraic form, exists_intCast_eq_factorial_mul_pow_mul_binomPolyCoeff, which says that

m! · (p-1)^m · β_{m,n}

is an integer. That is the honest content of the assertion that the coefficients lie in the subring generated by ℤ and 1/(p-1) — it exhibits the denominator explicitly as a power of p - 1 — it needs only p ≠ 1, and it is the form a consumer should reach for when a concrete denominator is more useful than a valuation bound. The valuation statement follows because p ∤ p - 1.

The algebraic form is proved by clearing all denominators at the level of polynomials: C (m! (p-1)^m) * B_m = ∏_{s<m} (X - 1 - s(p-1)), an identity between polynomials over ℚ verified pointwise with Polynomial.funext, whose right-hand side is visibly the image of a polynomial over ℤ.

The value at a power of p #

source
theorem GranvilleMoore.div_sub_one_eq_natCast_frobeniusExponent {p : ℕ} (hp : 2 ≤ p) (i : ℕ) :
(↑p ^ i - 1) / (↑p - 1) = ↑(frobeniusExponent p i)

The closed form of the Frobenius exponent as a rational number: (p^i - 1)/(p - 1) = e_i.

This is GranvilleMoore.sub_one_mul_frobeniusExponent_add_one divided by p - 1, and it is the substitution that makes B_m a binomial coefficient at z = p^i.

source
theorem GranvilleMoore.eval_binomPoly_pow_eq_choose {p : ℕ} (hp : 2 ≤ p) (m i : ℕ) :
Polynomial.eval (↑p ^ i) (binomPoly p m) = ↑((frobeniusExponent p i).choose m)

The binomial polynomial evaluates the binomial coefficient: B_m(p^i) = C(e_i, m), where e_i is the Frobenius exponent ∑_{r<i} p^r.

Substituting z = p^i sends (z-1)/(p-1) to e_i, so the defining product of B_m becomes the length-m falling factorial of e_i, and dividing it by m! is exactly C(e_i, m).

The expansion of the binomial coefficient #

source
theorem GranvilleMoore.natCast_choose_frobeniusExponent_eq_sum {p : ℕ} (hp : 2 ≤ p) (m i : ℕ) :
↑((frobeniusExponent p i).choose m) = ∑ n ∈ Finset.range (m + 1), binomPolyCoeff p m n * (↑p ^ n) ^ i

The binomial coefficient as a polynomial in p^i: C(e_i, m) = ∑_{n ≤ m} β_{m,n} (p^n)^i.

B_m has degree at most m, so it is ∑_{n ≤ m} β_{m,n} z^n; evaluating at z = p^i and using GranvilleMoore.eval_binomPoly_pow_eq_choose gives the claim, after rewriting (p^i)^n = (p^n)^i. The point of this shape is that the right-hand side is a fixed linear combination of the geometric progressions i ↦ (p^n)^i.

The denominators of the coefficients #

source
theorem GranvilleMoore.C_mul_binomPoly_eq_prod {p : ℕ} (hp : p ≠ 1) (m : ℕ) :
Polynomial.C (↑m.factorial * (↑p - 1) ^ m) * binomPoly p m = ∏ s ∈ Finset.range m, (Polynomial.X - 1 - Polynomial.C (↑s * (↑p - 1)))

The binomial polynomial with all denominators cleared: m! (p-1)^m B_m = ∏_{s<m} (X - 1 - s(p-1)).

Multiplying the defining product by (p-1)^m distributes one factor p - 1 into each of its m terms, turning (z-1)/(p-1) - s into z - 1 - s(p-1). The right-hand side has integer coefficients, which is the content of GranvilleMoore.exists_intCast_eq_factorial_mul_pow_mul_binomPolyCoeff.

source
theorem GranvilleMoore.exists_intCast_eq_factorial_mul_pow_mul_binomPolyCoeff {p : ℕ} (hp : p ≠ 1) (m n : ℕ) :
∃ (a : ℤ), ↑m.factorial * (↑p - 1) ^ m * binomPolyCoeff p m n = ↑a

The denominator of β_{m,n} is a power of p - 1: the rational number m! (p-1)^m β_{m,n} is an integer.

This is the algebraic form of the p-integrality of the coefficients: β_{m,n} lies in the subring of ℚ generated by ℤ, 1/m! and 1/(p-1), with the two denominators exhibited explicitly. Since p ∤ p - 1, it implies the valuation bound GranvilleMoore.neg_padicValRat_factorial_le_padicValRat_binomPolyCoeff.

source
theorem GranvilleMoore.padicValRat_natCast_sub_one {p : ℕ} (hp : Nat.Prime p) :
padicValRat p (↑p - 1) = 0

p - 1 is a p-adic unit: v_p(p - 1) = 0.

source
theorem GranvilleMoore.neg_padicValRat_factorial_le_padicValRat_binomPolyCoeff {p : ℕ} (hp : Nat.Prime p) (m n : ℕ) :
-padicValRat p ↑m.factorial ≤ padicValRat p (binomPolyCoeff p m n)

p-integrality of the coefficients: v_p(β_{m,n}) ≥ -v_p(m!).

The rational number m! (p-1)^m β_{m,n} is an integer, so has nonnegative valuation, and v_p((p-1)^m) = 0 because p ∤ p - 1; hence v_p(β_{m,n}) ≥ -v_p(m!). No bound relating n and m is needed: for n > m the coefficient vanishes and the inequality is trivial.

source
theorem GranvilleMoore.padicValRat_binomPolyCoeff_nonneg {p : ℕ} (hp : Nat.Prime p) {m : ℕ} (hm : m < p) (n : ℕ) :
0 ≤ padicValRat p (binomPolyCoeff p m n)

p-integrality of the coefficients, small m: v_p(β_{m,n}) ≥ 0 when m < p.

For m < p no factor of m! is divisible by p, so v_p(m!) = 0 and the bound of GranvilleMoore.neg_padicValRat_factorial_le_padicValRat_binomPolyCoeff becomes nonnegativity.