The iterated Fermat quotients

The objects of §3 of Granville's paper: the iterated Fermat quotients F^{(j)}_k(x), the coefficients c_{j,i}(p) of the falling p-power product, the unit quotient g_k(x), the rescaled binomial polynomial B_m with its coefficients β_{m,n}, and the collapsed coefficient A_j(m).

Everything here is a definition together with the API a consumer needs in order to use it without unfolding it. None of the definitions needs p to be prime, so none of them carries a primality hypothesis; the arithmetic lemmas that do are stated elsewhere.

All the divisions are taken in ℚ, so the definitions are total and unconditional; integrality is a theorem about them (GranvilleMoore.exists_intCast_iteratedFermatQuot and GranvilleMoore.unitQuot_eq_intCast), not part of their statement.

Main definitions

• GranvilleMoore.iteratedFermatQuot — F^{(j)}_k(x), the j-fold Fermat quotient.
• GranvilleMoore.cPoly, GranvilleMoore.cCoeff — ∏_{r<j}(X + p^r) and its coefficients c_{j,i}(p).
• GranvilleMoore.unitQuot — g_k(x) = (t_x^{p^k} - 1)/p^{k+1}, where t_x = x^{p-1}.
• GranvilleMoore.binomPoly, GranvilleMoore.binomPolyCoeff — B_m and β_{m,n}.
• GranvilleMoore.collapsedCoeff — A_j(m).

The iterated Fermat quotient

def GranvilleMoore.iteratedFermatQuot (p : ℕ) : ℕ → ℕ → ℤ → ℚ

The iterated Fermat quotient F^{(j)}_k(x) of Granville's paper: F^{(0)}_k(x) is x^(p^k), and F^{(j+1)}_k(x) is the divided difference (F^{(j)}_{k+1}(x) - F^{(j)}_k(x)) / p^(k+1).

The value is a rational number; that it is in fact an integer for prime p is GranvilleMoore.exists_intCast_iteratedFermatQuot. The recursion is on j, uniformly in k.

Equations

• GranvilleMoore.iteratedFermatQuot p 0 x✝¹ x✝ = ↑x✝ ^ p ^ x✝¹
• GranvilleMoore.iteratedFermatQuot p j.succ x✝¹ x✝ = (GranvilleMoore.iteratedFermatQuot p j (x✝¹ + 1) x✝ - GranvilleMoore.iteratedFermatQuot p j x✝¹ x✝) / ↑p ^ (x✝¹ + 1)

@[simp]

theorem GranvilleMoore.iteratedFermatQuot_zero (p k : ℕ) (x : ℤ) : iteratedFermatQuot p 0 k x = ↑x ^ p ^ k

The bottom of the tower: F^{(0)}_k(x) = x^(p^k).

@[simp]

theorem GranvilleMoore.iteratedFermatQuot_succ (p j k : ℕ) (x : ℤ) : iteratedFermatQuot p (j + 1) k x = (iteratedFermatQuot p j (k + 1) x - iteratedFermatQuot p j k x) / ↑p ^ (k + 1)

The divided-difference recursion: F^{(j+1)}_k(x) is (F^{(j)}_{k+1}(x) - F^{(j)}_k(x)) / p^(k+1).

The coefficients of the falling p-power product

noncomputable def GranvilleMoore.cPoly (p j : ℕ) : Polynomial ℤ

The falling p-power product ∏_{r<j}(X + p^r), whose coefficients are the c_{j,i}(p) of Granville's paper. The empty product for j = 0 is 1.

Equations

• GranvilleMoore.cPoly p j = ∏ r ∈ Finset.range j, (Polynomial.X + Polynomial.C (↑p ^ r))

noncomputable def GranvilleMoore.cCoeff (p j i : ℕ) : ℤ

The coefficient c_{j,i}(p) of X^i in ∏_{r<j}(X + p^r).

Equations

• GranvilleMoore.cCoeff p j i = (GranvilleMoore.cPoly p j).coeff i

@[simp]

theorem GranvilleMoore.cPoly_zero (p : ℕ) : cPoly p 0 = 1

The empty falling p-power product is 1.

theorem GranvilleMoore.cPoly_succ (p j : ℕ) : cPoly p (j + 1) = cPoly p j * (Polynomial.X + Polynomial.C (↑p ^ j))

The falling p-power product gains the factor X + p^j at step j.

theorem GranvilleMoore.monic_cPoly (p j : ℕ) : (cPoly p j).Monic

The falling p-power product is monic, being a product of monic linear factors.

@[simp]

theorem GranvilleMoore.natDegree_cPoly (p j : ℕ) : (cPoly p j).natDegree = j

The falling p-power product ∏_{r<j}(X + p^r) has degree j.

theorem GranvilleMoore.cCoeff_eq_zero_of_lt {p j i : ℕ} (h : j < i) : cCoeff p j i = 0

The coefficients c_{j,i}(p) vanish above the degree: c_{j,i}(p) = 0 for i > j.

@[simp]

theorem GranvilleMoore.cCoeff_self (p j : ℕ) : cCoeff p j j = 1

The top coefficient of the falling p-power product is 1: the product is monic of degree j.

theorem GranvilleMoore.cPoly_eq_sum (p j : ℕ) : cPoly p j = ∑ i ∈ Finset.range (j + 1), Polynomial.C (cCoeff p j i) * Polynomial.X ^ i

The defining identity of the coefficients c_{j,i}(p), in the form ∏_{r<j}(X + p^r) = ∑_{i ≤ j} c_{j,i}(p) X^i.

The unit quotient

def GranvilleMoore.unitQuot (p : ℕ) (x : ℤ) (k : ℕ) : ℚ

The unit quotient g_k(x) = (t_x^{p^k} - 1) / p^{k+1} of Granville's paper, where t_x = x^{p-1}; equivalently (x^{(p-1)p^k} - 1)/p^{k+1}.

The value is a rational number; that it is in fact an integer for an odd prime p not dividing x is GranvilleMoore.unitQuot_eq_intCast.

Equations

• GranvilleMoore.unitQuot p x k = ↑(x ^ ((p - 1) * p ^ k) - 1) / ↑p ^ (k + 1)

theorem GranvilleMoore.unitQuot_eq (p : ℕ) (x : ℤ) (k : ℕ) : unitQuot p x k = ↑((x ^ (p - 1)) ^ p ^ k - 1) / ↑p ^ (k + 1)

g_k(x) written with the unit t_x = x^{p-1} visible.

@[simp]

theorem GranvilleMoore.unitQuot_zero (p : ℕ) (x : ℤ) : unitQuot p x 0 = ↑(x ^ (p - 1) - 1) / ↑p

The bottom unit quotient is the Fermat quotient: g_0(x) = (x^{p-1} - 1)/p.

theorem GranvilleMoore.pow_eq_one_add_pow_mul_unitQuot {p : ℕ} (hp : p ≠ 0) (x : ℤ) (k : ℕ) : (↑x ^ (p - 1)) ^ p ^ k = 1 + ↑p ^ (k + 1) * unitQuot p x k

The characterising property of g_k(x): t_x^{p^k} = 1 + p^{k+1} g_k(x), as an identity in ℚ. This is the form consumers rewrite with, so that unitQuot never has to be unfolded.

The binomial polynomial and its coefficients

noncomputable def GranvilleMoore.binomPoly (p m : ℕ) : Polynomial ℚ

The rescaled binomial polynomial B_m(z) = (1/m!) ∏_{s<m} ((z-1)/(p-1) - s) of Granville's paper, the empty product for m = 0 being 1. It is built from descPochhammer ℚ m = ∏_{s<m}(X - s) by substituting (z-1)/(p-1); eval_binomPoly recovers the product formula.

Equations

• GranvilleMoore.binomPoly p m = (↑m.factorial)⁻¹ • (descPochhammer ℚ m).comp ((↑p - 1)⁻¹ • (Polynomial.X - 1))

noncomputable def GranvilleMoore.binomPolyCoeff (p m n : ℕ) : ℚ

The coefficient β_{m,n} of z^n in B_m. It vanishes for n > m (binomPolyCoeff_eq_zero_of_lt), so no bound on n is built into the definition.

Equations

• GranvilleMoore.binomPolyCoeff p m n = (GranvilleMoore.binomPoly p m).coeff n

@[simp]

theorem GranvilleMoore.binomPoly_zero (p : ℕ) : binomPoly p 0 = 1

The empty rescaled binomial polynomial is 1.

theorem GranvilleMoore.eval_binomPoly (p m : ℕ) (z : ℚ) : Polynomial.eval z (binomPoly p m) = (↑m.factorial)⁻¹ * ∏ s ∈ Finset.range m, ((z - 1) / (↑p - 1) - ↑s)

The product formula for B_m: B_m(z) = (1/m!) ∏_{s<m} ((z-1)/(p-1) - s).

theorem GranvilleMoore.natDegree_binomPoly_le (p m : ℕ) : (binomPoly p m).natDegree ≤ m

The rescaled binomial polynomial B_m has degree at most m, being a rescaled composition of a degree-m polynomial with a linear one.

theorem GranvilleMoore.binomPolyCoeff_eq_zero_of_lt {p m n : ℕ} (h : m < n) : binomPolyCoeff p m n = 0

The coefficients of B_m vanish above the degree: β_{m,n} = 0 for n > m.

theorem GranvilleMoore.binomPoly_eq_sum (p m : ℕ) : binomPoly p m = ∑ n ∈ Finset.range (m + 1), Polynomial.C (binomPolyCoeff p m n) * Polynomial.X ^ n

B_m is the polynomial with coefficients β_{m,n} for n ≤ m.

The collapsed coefficient

noncomputable def GranvilleMoore.collapsedCoeff (p j m : ℕ) : ℚ

The collapsed coefficient A_j(m) = ∑_{i ≤ j} (-1)^{j-i} c_{j,i}(p) * (e_i choose m) of Granville's paper, where e_i = ∑_{r<i} p^r is the Frobenius exponent GranvilleMoore.frobeniusExponent p i, written out here and definitionally equal to it.

It is rational because it is compared with p-adic valuations and combined with rational quantities in the master expansion GranvilleMoore.iteratedFermatQuot_eq_mul_sum, even though the summands are integers. Its content is in GranvilleMoore.collapsedCoeff_eq_sum, GranvilleMoore.collapsedCoeff_eq_zero, GranvilleMoore.le_padicValRat_collapsedCoeff and GranvilleMoore.collapsedCoeff_self_eq.

Equations

• GranvilleMoore.collapsedCoeff p j m = ∑ i ∈ Finset.range (j + 1), (-1) ^ (j - i) * ↑(GranvilleMoore.cCoeff p j i) * ↑((∑ r ∈ Finset.range i, p ^ r).choose m)

@[simp]

theorem GranvilleMoore.collapsedCoeff_zero_left (p m : ℕ) : collapsedCoeff p 0 m = if m = 0 then 1 else 0

The collapsed coefficient at j = 0 is the indicator of m = 0: A_0(m) is 1 for m = 0 and 0 otherwise.