Lemma 4.1 for Thakur's hypotheses on power sums #
Encoding of the Laurent field F_q((1/t)) #
We model F_q((1/t)) by LaurentSeries Fq = HahnSeries ℤ Fq, in which the
formal variable X plays the role of the uniformizer 1/t. Thus t corresponds
to X⁻¹, and the coefficient of Xⁿ of an element is precisely the coefficient
of t ^ {-n} in its expansion in descending powers of t.
The F_q-algebra embedding F_q[t] → F_q((1/t)) sending t ↦ X⁻¹, i.e. the
expansion of a polynomial in descending powers of t. Since F_q((1/t)) is a
field, this extends multiplicatively to inverses, which is how a ^ {-k} is
interpreted below.
Equations
Instances For
Definition 1 (Carry-free addition in base p).
The addition of the nonnegative integers in xs is carry-free in base p if for
every digit position e, the sum of the e-th base-p digits is at most
p - 1.
Equations
- ZetaH123.Lem41.CarryFree p xs = ∀ (e : ℕ), (List.map (fun (x : ℕ) => ZetaH123.Lem41.digit p x e) xs).sum ≤ p - 1
Instances For
The monic polynomial of degree exactly d with prescribed lower coefficients
θ : Fin d → Fq, namely t ^ d + ∑_{i<d} (θ i) t ^ i. As θ ranges over
Fin d → Fq this enumerates the set A_d ^ + of monic polynomials of degree d
without repetition (see monicOf_monic/monicOf_natDegree/monicOf_injective).
Equations
- ZetaH123.Lem41.monicOf Fq d θ = Polynomial.X ^ d + ∑ i : Fin d, Polynomial.C (θ i) * Polynomial.X ^ ↑i
Instances For
Definition 3 (The power sum S_d(k)).
S_d(k) = ∑_{a ∈ A_d ^ +} a ^ {-k}, summed over the monic polynomials of degree d
(parameterized by their lower coefficients θ : Fin d → Fq), viewed as an
element of F_q((1/t)) via the embedding phi. The inverse (phi a)⁻¹ is taken
in the Laurent series field, which realizes the expansion of a ^ {-1} in
descending powers of t.
Equations
- ZetaH123.Lem41.Sdk Fq d k = ∑ θ : Fin d → Fq, ((ZetaH123.Lem41.phi Fq) (ZetaH123.Lem41.monicOf Fq d θ))⁻¹ ^ k
Instances For
The explicit witness family c_m #
For a tuple m = (m_1,…,m_d) with y := ∑_i m_i, the witness coefficient is
c_m = (-1) ^ d · (-1) ^ y · C(k+y-1, y) · multinomial(y; m_1,…,m_d) (mod p),
where the global factor (-1) ^ d comes from ∑_{x∈F_q} x ^ {m_i} = -1 for each of
the d variables.
The explicit witness family. For m : Fin d → ℕ, with y = ∑ i, m i,
cwit Fq k m is the F_q-image of the integer
(-1) ^ d · (-1) ^ y · C(k + y - 1, y) · multinomial(y; m).
Equations
- ZetaH123.Lem41.cwit Fq d k m = ↑(((-1) ^ d * (-1) ^ ∑ i : Fin d, m i) * ↑((k + ∑ i : Fin d, m i - 1).choose (∑ i : Fin d, m i)) * ↑(Nat.multinomial Finset.univ m))
Instances For
Sub-lemmas of the structure theorem #
The proof of main factors through: L1 (Sdk_coeff_as_thetasum), the
Laurent/multinomial expansion of coeff n (Sdk); L2 (finField_pow_sum), the
finite-field power sum collapsing the θ-sum; L3/L4
(negChoose_cast_ne_zero_iff/multinomial_cast_ne_zero_iff), Lucas-type
nonvanishing criteria; L5 (carryfree_combine), combining the carry-free
conditions; then the assembly lemmas cwit_ne_zero and Sdk_coeff_eq_finsum.
L3 (Lucas, binomial). The integer binom(-k, y) = (-1) ^ y · C(k+y-1, y)
has nonzero image in F_q (char p) iff the addition (k - 1) + y is carry-free
in base p, i.e. CarryFree p [k-1, y] (Kummer/Lucas).
L4 (Lucas, multinomial). With y = ∑ i, m i, the multinomial coefficient
multinomial(y; m_1,…,m_d) has nonzero image in F_q iff the addition
m_1 ⊕ m_2 ⊕ … ⊕ m_d is carry-free in base p, i.e. CarryFree p (List.ofFn m).
(Telescoping product of binomial-Lucas, informal.tex Lemma 1.6.)
Crux (division form). If, at every base-p digit position, the digits of a
and b sum to at most p - 1 (no carry), then dividing by p ^ e distributes
over the sum a + b. Requires 1 < p.
Crux (list form, all p). If the addition of the entries of L is carry-free
in base p, then for every digit position the digit of L.sum equals the sum of
the digits of the entries. (Holds unconditionally for p ≤ 1.)
L5 (carry-free combination). With y = ∑ i, m i, the two carry-free
conditions CarryFree p [k-1, y] (binomial) and CarryFree p (List.ofFn m)
(multinomial) hold simultaneously iff the combined addition is carry-free, i.e.
CarryFree p ((k - 1) :: List.ofFn m).
L1 helper lemmas (PowerSeries / LaurentSeries infrastructure) #
The proof of L1 (Sdk_coeff_as_thetasum) is decomposed into helper lemmas H1–H5:
H1 is the generalized binomial / unit-inverse power-series expansion; H2–H4 are
the phi/monicOf → LaurentSeries bridge and the HahnSeries shift; H5 is the
finite-vs-finsum bookkeeping.
H1 (generalized binomial / unit-inverse power-series expansion). For a
power series g with zero constant term, the e-th coefficient of
((1 + g) ^ k)⁻¹ is the finite sum ∑_{y ≤ e} binom(-k, y) · coeff_e (g ^ y),
where binom(-k, y) = (-1) ^ y · C(k+y-1, y). (Only y ≤ e contribute since
order (g ^ y) ≥ y.)
H2 (phi (monicOf θ) made explicit). phi (monicOf θ) equals the shift
single (-d) 1 times the coercion of the unit power series
1 + ∑_{i<d} θ_i X ^ {d-i}. (phi = aeval X⁻¹, X⁻¹ = single (-1) 1; pull out
single (-d) 1 and identify the bracket with the coerced power series.)
H3 (inverse k-th power as shift × PowerSeries inverse). From H2: the
k-th power of the inverse is single (d*k) 1 times the coercion of the
PowerSeries inverse ((1 + g) ^ k)⁻¹, where g = ∑_{i<d} θ_i X ^ {d-i}. Uses that a
power series with constant term 1 is a unit, so (↑u)⁻¹ = ↑(u⁻¹) in
LaurentSeries.
H4 (coefficient of single s 1 * ↑f, the Laurent shift). The n-th
coefficient of single s 1 * (↑f) is the (n-s)-th PowerSeries coefficient of
f when n - s ≥ 0, else 0.
H5 (per-θ coefficient identity). Assembling H1 (binomial expansion),
the multinomial theorem (Finset.sum_pow_eq_sum_piAntidiag for g ^ y), and the
re-indexing of the X ^ {d-i} exponents against weight d m = ∑ (i+1) m_i, the
coefficient of X ^ n in (phi (monicOf θ))⁻¹ ^ k is the finsum over tuples m with
d*k + weight(m) = n of binom(-k, ∑ m_i)·multinomial·∏ θ_i ^ {m_i}.
L1 (Laurent/multinomial expansion). The coefficient of X ^ n in Sdk
equals the θ-sum of single-monic-polynomial coefficients, each of which is the
finite tuple-sum of binom(-k,y)·multinomial(y;m)·∏_i (θ i) ^ {m i} over tuples m
with d*k + w(m) = n.
Assembly (b): nonvanishing of cwit on the index set. For m ∈ T_{d,k-1},
cwit Fq d k m ≠ 0. From L3, L4, and L5: membership in Tindex supplies both
carry-free conditions, and the global (-1) ^ d is a unit.
Assembly (c): the coefficient identity with the explicit witness cwit.
Combines L1 (expansion), L2 (the finite-field power sum collapsing the θ-sum to
(-1) ^ d exactly when every m i > 0 ∧ (q - 1) ∣ m i), and L3/L4/L5 (a term has
nonzero coefficient iff m ∈ Tindex), regrouped as the finsum of cwit over the
admissible fiber {m ∈ Tindex | d*k + w(m) = n}.
Theorem.
There exists a family of scalars c_m ∈ F_q indexed by d-tuples m, all
nonzero on the index set T_{d,k-1}, such that
S_d(k) = t ^ {-dk} ∑_{m ∈ T_{d,k-1}} c_m t ^ {-w(m)}.
The identity is expressed coefficient-by-coefficient in F_q((1/t)): working with
the uniformizer X = 1/t, the coefficient of Xⁿ (equivalently of t ^ {-n}) in
S_d(k) equals the sum of c_m over the (finite) set of tuples m ∈ T_{d,k-1}
with d*k + w(m) = n. This faithfully captures that the right-hand side is a
formal sum of monomials t ^ {-w(m)} indexed by the tuples (with repetition
allowed): each individual c_m is nonzero, while the collected coefficient of a
given power of t may vanish.
Correctness statements for the definitions #
The following auxiliary statements pin down that monicOf is the intended
enumeration of the monic polynomials of degree exactly d, justifying that
Sdk is the power sum S_d(k) = ∑_{a ∈ A_d ^ +} a ^ {-k}.
Distinct coefficient tuples give distinct polynomials, so the parameterization
of A_d ^ + by Fin d → Fq has no repetitions.
The parameterization is surjective onto A_d ^ +: every monic polynomial of
degree exactly d arises as monicOf of its lower coefficients.