Stepanov's square-root point-count bound

The nonzero auxiliary polynomials and their proved Hasse multiplicities give the one-sided counts in Harcos (13). The quadratic character then converts these bounds into the affine point count in Theorem 7.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovLocus {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (f : Polynomial F) (a : F) : Finset F

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovLocus f a = {x : F | Polynomial.eval x f = 0 ∨ Polynomial.eval x f ^ ((Fintype.card F - 1) / 2) = a}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_locus_card_lt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (f : Polynomial F) (a : F) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hm : 3 ≤ f.natDegree) (hmq : 6 * f.natDegree < Fintype.card F) : ↑(stepanovLocus f a).card < ↑(Fintype.card F) / 2 + 2 * ↑f.natDegree * ↑(stepanovEll (Fintype.card F))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_quadraticChar_sum_bound_of_eval_zero_ne {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (f : Polynomial F) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hm : 3 ≤ f.natDegree) (hmq : 6 * f.natDegree < Fintype.card F) : |∑ x : F, ↑((quadraticChar F) (Polynomial.eval x f))| < 4 * ↑f.natDegree * ↑(stepanovEll (Fintype.card F))

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovPointCount {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (f : Polynomial F) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovPointCount f = {xy : F × F | xy.2 ^ 2 = Polynomial.eval xy.1 f}.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovPointCount_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (f : Polynomial F) (hq : Odd (Fintype.card F)) : ↑(stepanovPointCount f) = ↑(Fintype.card F) + ∑ x : F, ↑((quadraticChar F) (Polynomial.eval x f))

The affine point count is exactly q plus the quadratic-character sum.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_pointCount_bound_of_eval_zero_ne {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (f : Polynomial F) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hm : 3 ≤ f.natDegree) (hmq : 6 * f.natDegree < Fintype.card F) : |↑(stepanovPointCount f) - ↑(Fintype.card F)| < 4 * ↑f.natDegree * ↑⌈√↑(Fintype.card F)⌉₊

Harcos Theorem 7 with the harmless normalization f(0) ≠ 0 still explicit.