Vanishing of the actual Stepanov auxiliary polynomial

This is the passage from (20) to (22) on printed page 11 of Harcos, Weil's bound for Kloosterman sums (pages/harcos-stepanov-11.png). Frobenius kills the positive Hasse derivatives of X^(jq) below order q. Factoring out f^(ell-k) additionally requires k ≤ ell; the vanishing application uses k < ell ≤ q.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_hasseDeriv_X_card_mul {F : Type u_1} [Field F] [Fintype F] (j k : ℕ) (hk : 0 < k) (hkq : k < Fintype.card F) : (Polynomial.hasseDeriv k) (Polynomial.X ^ (j * Fintype.card F)) = 0

Frobenius forces every positive Hasse derivative of X^(jq) below order q to vanish as a polynomial, not just as a function on the field. The Frobenius residue of ((X + 1)^j)^q determines its low Taylor coefficients; evaluating a Hasse monomial at 1 recovers its sole coefficient.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_hasseDeriv_mul_X_card_mul {F : Type u_1} [Field F] [Fintype F] (g : Polynomial F) (j k : ℕ) (hkq : k < Fintype.card F) : (Polynomial.hasseDeriv k) (g * Polynomial.X ^ (j * Fintype.card F)) = (Polynomial.hasseDeriv k) g * Polynomial.X ^ (j * Fintype.card F)

Below order q, a factor X^(jq) is constant for Hasse differentiation.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_hasseDeriv_pow_mul_ansatz {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (hf : f ≠ 0) (ell k : ℕ) {J : ℕ} (r s : Fin J → Polynomial F) (hk : k ≤ ell) (hkq : k < Fintype.card F) : (Polynomial.hasseDeriv k) (f ^ ell * stepanovAnsatz f r s) = f ^ (ell - k) * ∑ j : Fin J, ((stepanovHasseOperator f hf ell k) (r j) + (stepanovHasseOperator f hf (ell + (Fintype.card F - 1) / 2) k) (s j) * f ^ ((Fintype.card F - 1) / 2)) * Polynomial.X ^ (↑j * Fintype.card F)

Equation (20), with the necessary extraction range k ≤ ell.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_hasseDeriv_pow_mul_ansatz_eval {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (hf : f ≠ 0) (ell k : ℕ) {J : ℕ} (r s : Fin J → Polynomial F) (a x : F) (hk : k < ell) (hell : ell ≤ Fintype.card F) (hx : Polynomial.eval x f ^ ((Fintype.card F - 1) / 2) = a) : Polynomial.eval x ((Polynomial.hasseDeriv k) (f ^ ell * stepanovAnsatz f r s)) = Polynomial.eval x f ^ (ell - k) * Polynomial.eval x (stepanovConstraint f hf ell ((Fintype.card F - 1) / 2) a k r s)

Evaluating (20) at f(x)^((q-1)/2) = a gives precisely (22).

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_hasseDeriv_pow_mul_eval_zero {F : Type u_1} [Field F] (f g : Polynomial F) (ell k : ℕ) (x : F) (hk : k < ell) (hx : Polynomial.eval x f = 0) : Polynomial.eval x ((Polynomial.hasseDeriv k) (f ^ ell * g)) = 0

At a zero of f, the multiplier f^ell itself supplies all required Hasse vanishing, independently of the coefficient equations.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_constraints_imply_hasse_vanishing {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (hf : f ≠ 0) (ell : ℕ) {J : ℕ} (r s : Fin J → Polynomial F) (a : F) (hell : ell ≤ Fintype.card F) (hc : ∀ k < ell, stepanovConstraint f hf ell ((Fintype.card F - 1) / 2) a k r s = 0) (x : F) : Polynomial.eval x f = 0 ∨ Polynomial.eval x f ^ ((Fintype.card F - 1) / 2) = a → ∀ k < ell, Polynomial.eval x ((Polynomial.hasseDeriv k) (f ^ ell * stepanovAnsatz f r s)) = 0

The actual equation system (22) forces Hasse vanishing of the actual auxiliary polynomial at the union of the two specified loci.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovAnsatz_degree_lt {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) {J B : ℕ} (r s : Fin J → Polynomial F) (hr : ∀ (j : Fin J), (r j).degree < ↑B) (hs : ∀ (j : Fin J), (s j).degree < ↑B) : (stepanovAnsatz f r s).degree < ↑(B + (Fintype.card F - 1) / 2 * f.natDegree + (J - 1) * Fintype.card F)

Degree of the block ansatz, including the empty family and zero coefficients. The strict degree convention also covers B = 0.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_pow_mul_ansatz_degree_lt {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (ell : ℕ) {J B : ℕ} (r s : Fin J → Polynomial F) (hr : ∀ (j : Fin J), (r j).degree < ↑B) (hs : ∀ (j : Fin J), (s j).degree < ↑B) : (f ^ ell * stepanovAnsatz f r s).degree < ↑(B + (Fintype.card F - 1) / 2 * f.natDegree + (J - 1) * Fintype.card F + ell * f.natDegree)

Degree budget for the actual auxiliary polynomial used in point counting.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_exists_auxiliary_polynomial {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (ell B J : ℕ) (a : F) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hm : 1 ≤ f.natDegree) (hJ : 0 < J) (hell : ell ≤ Fintype.card F) (hB : 2 * (B - 1) + f.natDegree < Fintype.card F) (hcount : ∑ k : Fin ell, (B + ↑k * (f.natDegree - 1) + (J - 1)) < 2 * J * B) : ∃ (h : Polynomial F), h ≠ 0 ∧ h.degree < ↑(B + (Fintype.card F - 1) / 2 * f.natDegree + (J - 1) * Fintype.card F + ell * f.natDegree) ∧ ∀ (x : F), Polynomial.eval x f = 0 ∨ Polynomial.eval x f ^ ((Fintype.card F - 1) / 2) = a → ∀ k < ell, Polynomial.eval x ((Polynomial.hasseDeriv k) h) = 0

Harcos's auxiliary polynomial exists from the actual dimension inequality, with nonvanishing, degree control, and genuine Hasse vanishing.