Nonvanishing of the Stepanov auxiliary polynomial

The argument is the first half of printed page 11 of Gergely Harcos, Weil's bound for Kloosterman sums (pages/harcos-stepanov-11.png).

The nonsquare hypothesis is geometric: it concerns the polynomial after base change to the algebraic closure, not just squares over the finite field.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_sq_mul_eq_const_mul_sq {F : Type u_1} [Field F] (f r s : Polynomial F) (c : F) (hc : c ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (h : r ^ 2 * f = s ^ 2 * Polynomial.C c) : r = 0 ∧ s = 0

The geometric nonsquare obstruction used after reducing modulo X^q.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_X_card_dvd_pow_sub_const {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) : Polynomial.X ^ Fintype.card F ∣ f ^ Fintype.card F - Polynomial.C (Polynomial.eval 0 f)

Frobenius makes the constant term the entire residue of f^q modulo X^q.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_block_eq_zero_of_X_card_dvd {F : Type u_1} [Field F] [Fintype F] (f r s : Polynomial F) (B : ℕ) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hr : r.degree < ↑B) (hs : s.degree < ↑B) (hB : 2 * (B - 1) + f.natDegree < Fintype.card F) (hdiv : Polynomial.X ^ Fintype.card F ∣ r + s * f ^ ((Fintype.card F - 1) / 2)) : r = 0 ∧ s = 0

Harcos's residue kernel lemma: a degree-bounded block cannot be divisible by X^q. The degree convention includes zero polynomials even when B = 0.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovAnsatz {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) {J : ℕ} (r s : Fin J → Polynomial F) : Polynomial F

The actual Stepanov block ansatz, before multiplication by f^ell.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovAnsatz f r s = ∑ j : Fin J, (r j + s j * f ^ ((Fintype.card F - 1) / 2)) * Polynomial.X ^ (↑j * Fintype.card F)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovAnsatz_coefficients_eq_zero {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) {J B : ℕ} (r s : Fin J → Polynomial F) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hr : ∀ (j : Fin J), (r j).degree < ↑B) (hs : ∀ (j : Fin J), (s j).degree < ↑B) (hB : 2 * (B - 1) + f.natDegree < Fintype.card F) (hz : stepanovAnsatz f r s = 0) (j : Fin J) : r j = 0 ∧ s j = 0

All coefficients vanish if the actual Stepanov ansatz vanishes. Successively removing the first block is equivalent to Harcos's choice of the least nonzero block.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovAnsatz_eq_iff {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) {J B : ℕ} (r s r' s' : Fin J → Polynomial F) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hr : ∀ (j : Fin J), (r j).degree < ↑B) (hs : ∀ (j : Fin J), (s j).degree < ↑B) (hr' : ∀ (j : Fin J), (r' j).degree < ↑B) (hs' : ∀ (j : Fin J), (s' j).degree < ↑B) (hB : 2 * (B - 1) + f.natDegree < Fintype.card F) : stepanovAnsatz f r s = stepanovAnsatz f r' s' ↔ r = r' ∧ s = s'

Injectivity of the actual ansatz on degree-bounded coefficient families.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovAnsatz_ne_zero {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) {J B : ℕ} (r s : Fin J → Polynomial F) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hr : ∀ (j : Fin J), (r j).degree < ↑B) (hs : ∀ (j : Fin J), (s j).degree < ↑B) (hB : 2 * (B - 1) + f.natDegree < Fintype.card F) (hne : ∃ (j : Fin J), r j ≠ 0 ∨ s j ≠ 0) : stepanovAnsatz f r s ≠ 0

Harcos page 11: a nontrivial bounded coefficient family gives a nonzero auxiliary polynomial, under the geometric nonsquare hypothesis.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_pow_mul_ansatz_ne_zero {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (ell : ℕ) {J B : ℕ} (r s : Fin J → Polynomial F) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hr : ∀ (j : Fin J), (r j).degree < ↑B) (hs : ∀ (j : Fin J), (s j).degree < ↑B) (hB : 2 * (B - 1) + f.natDegree < Fintype.card F) (hne : ∃ (j : Fin J), r j ≠ 0 ∨ s j ≠ 0) : f ^ ell * stepanovAnsatz f r s ≠ 0

The same nonvanishing conclusion after the multiplier in Harcos's ansatz.