Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system, Mathlib version, quality requirements and compilation performance.

Hasse derivatives and multiplicities

Proves the Hasse-derivative root criterion, multiplicity bounds, and degree control for auxiliary-polynomial derivatives. Reference: Harcos (2015), §4, equations (14)–(15) and Lemmas 8–10; Stepanov (1972).

theorem KloostermanWeil.Stepanov.hasseRootMultiplicityCriterion {F : Type u_1} [Field F] (h : Polynomial F) (x : F) (l : ℕ) : (Polynomial.X - Polynomial.C x) ^ l ∣ h ↔ ∀ k < l, Polynomial.eval x ((Polynomial.hasseDeriv k) h) = 0

A point has multiplicity at least l exactly when its first l Hasse derivatives vanish. This is Stepanov's Hasse-derivative criterion.

theorem KloostermanWeil.Stepanov.card_mul_le_natDegree_of_uniform_rootMultiplicity {F : Type u_1} [Field F] (h : Polynomial F) (hh : h ≠ 0) (S : Finset F) {l : ℕ} (hl : 0 < l) (hS : ∀ x ∈ S, (Polynomial.X - Polynomial.C x) ^ l ∣ h) : l * S.card ≤ h.natDegree

If every point in S is a root of multiplicity at least l of a nonzero polynomial, then l * #S is at most its degree. This is the exact counting step in Stepanov inequality (14).

theorem KloostermanWeil.Stepanov.pow_sub_dvd_hasseDeriv_mul_pow {F : Type u_1} [Field F] (f g : Polynomial F) {n k : ℕ} (hk : k ≤ n) : f ^ (n - k) ∣ (Polynomial.hasseDeriv k) (g * f ^ n)

The kth Hasse derivative of g * f^n retains at least n-k factors of f. This is the divisibility part of Stepanov's Lemma 10.

theorem KloostermanWeil.Stepanov.hasseDeriv_mul_pow_factor_degree {F : Type u_1} [Field F] (f g : Polynomial F) (hf : f ≠ 0) (hfdeg : 0 < f.natDegree) {n k : ℕ} (hk : k ≤ n) : ∃ (u : Polynomial F), (Polynomial.hasseDeriv k) (g * f ^ n) = f ^ (n - k) * u ∧ u.natDegree + k ≤ g.natDegree + k * f.natDegree

Cancellation-safe form of the degree conclusion in Stepanov's Lemma 10. The displayed inequality is equivalent to deg u ≤ deg g + k * deg f - k.

noncomputable def KloostermanWeil.Stepanov.hassePowerQuotient {F : Type u_1} [Field F] (f : Polynomial F) {n k : ℕ} (hk : k ≤ n) (g : Polynomial F) : Polynomial F

Canonical quotient after removing the guaranteed factor f^(n-k) from the Hasse derivative.

Equations

• KloostermanWeil.Stepanov.hassePowerQuotient f hk g = Classical.choose ⋯

theorem KloostermanWeil.Stepanov.hassePowerQuotient_spec {F : Type u_1} [Field F] (f : Polynomial F) {n k : ℕ} (hk : k ≤ n) (g : Polynomial F) : (Polynomial.hasseDeriv k) (g * f ^ n) = f ^ (n - k) * hassePowerQuotient f hk g

Exact factorization defining hassePowerQuotient.

noncomputable def KloostermanWeil.Stepanov.hassePowerQuotientLinearMap {F : Type u_1} [Field F] (f : Polynomial F) (hf : f ≠ 0) {n k : ℕ} (hk : k ≤ n) : Polynomial F →ₗ[F] Polynomial F

For fixed f, n, and k, the quotient in Stepanov's Lemma 10 depends linearly on g.

Equations

• KloostermanWeil.Stepanov.hassePowerQuotientLinearMap f hf hk = { toFun := KloostermanWeil.Stepanov.hassePowerQuotient f hk, map_add' := ⋯, map_smul' := ⋯ }

theorem KloostermanWeil.Stepanov.hassePowerQuotient_natDegree {F : Type u_1} [Field F] (f g : Polynomial F) (hf : f ≠ 0) (hfdeg : 0 < f.natDegree) {n k : ℕ} (hk : k ≤ n) : (hassePowerQuotient f hk g).natDegree + k ≤ g.natDegree + k * f.natDegree

Degree bound for the canonical quotient, in the cancellation-safe form of Stepanov's inequality (16).

theorem KloostermanWeil.Stepanov.prime_dvd_choose_mul_prime_pow {p : ℕ} (hp : Nat.Prime p) (n j k : ℕ) (hk0 : 0 < k) (hk : k < p ^ n) : p ∣ (j * p ^ n).choose k

Lucas-theorem divisibility needed to show that the kth Hasse derivative does not see an X^(j*q) block when q is a prime power and 0 < k < q.

theorem KloostermanWeil.Stepanov.hasseDeriv_X_mul_prime_pow_eq_zero {F : Type u_1} [Field F] {p n j k : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hk0 : 0 < k) (hk : k < p ^ n) : (Polynomial.hasseDeriv k) (Polynomial.X ^ (j * p ^ n)) = 0

A positive Hasse derivative below q=p^n annihilates every Frobenius block X^(j*q).

theorem KloostermanWeil.Stepanov.hasseDeriv_mul_X_mul_prime_pow {F : Type u_1} [Field F] {p n j k : ℕ} [Fact (Nat.Prime p)] [CharP F p] (hk : k < p ^ n) (g : Polynomial F) : (Polynomial.hasseDeriv k) (g * Polynomial.X ^ (j * p ^ n)) = (Polynomial.hasseDeriv k) g * Polynomial.X ^ (j * p ^ n)

Below the prime-power block size, Hasse differentiation acts only on the coefficient polynomial in g * X^(j*q). This is the exact identity used to pass from equation (18) to equation (20).