The explicit form of the iterated Fermat quotients

The divided-difference recursion defining iteratedFermatQuot is unrolled once and for all: F^{(j)}_k(x) is a single fraction whose numerator is the signed combination of the powers x^{p^{k+i}} weighted by the coefficients c_{j,i}(p) of the falling p-power product, and whose denominator is p^{jk + C(j+1,2)}.

Main results

• GranvilleMoore.iteratedFermatQuot_eq_sum_div: the explicit form F^{(j)}_k(x) = (∑_{i ≤ j} (-1)^{j-i} c_{j,i}(p) x^{p^{k+i}}) / p^{jk + C(j+1,2)}.

Implementation notes

The induction is on j uniformly in k, since the divided difference needs the formula at both k and k+1; generalizing k supplies the quantified inductive hypothesis.

The combinatorial half of the step — that the numerator at level j+1 is the numerator at level j shifted in k minus p^j times the unshifted one — is isolated in numerator_recursion, so that the main proof is only the bookkeeping of a common denominator. That isolation matters: the shift is an index reindexing whose boundary term at i = 0 is supplied by cCoeff_succ_zero, while the interior is cCoeff_succ, and mixing that with the division would make one indivisible mess.

The exponent identity behind the common denominator is (j+1)(k+1) + C(j+1,2) = (j+1)k + C(j+2,2), which is C(j+2,2) = C(j+1,2) + (j+1); it is proved from Nat.choose_succ_succ rather than Nat.choose_two_right, whose division by two is gratuitous here.

The constant coefficient of the falling p-power product

The numerator recursion

The explicit form

theorem GranvilleMoore.iteratedFermatQuot_eq_sum_div {p : ℕ} (hp : p ≠ 0) (j k : ℕ) (x : ℤ) : iteratedFermatQuot p j k x = (∑ i ∈ Finset.range (j + 1), (-1) ^ (j - i) * ↑(cCoeff p j i) * ↑x ^ p ^ (k + i)) / ↑p ^ (j * k + (j + 1).choose 2)

prop_fermatexplicit: the explicit form of the iterated Fermat quotient,

F^{(j)}_k(x) = (1 / p^{jk + C(j+1,2)}) * ∑_{i=0}^{j} (-1)^{j-i} c_{j,i}(p) x^{p^{k+i}} .

Induction on j, uniformly in k. The base case is the empty product c_{0,0}(p) = 1 over the empty denominator; the step puts the two halves of the divided difference over the common denominator p^{(j+1)(k+1) + C(j+1,2)} = p^{(j+1)k + C(j+2,2)} and appeals to numerator_recursion.