Harcos's affine curve

The final paragraph of Harcos, page 12 (pages/harcos-weil-12.png), applies Theorem 7 to (X^p - X)^2 - 4ab. The geometric nonsquareness below follows the source's factorization argument, rather than assuming a curve estimate. The count is the actual affine count, not the count of a projective completion. The final section removes the auxiliary normalization f(0) ≠ 0 by translation, giving Theorem 7 in its original domain.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePolynomial {K : Type u_1} [Field K] (p : ℕ) (a b : K) : Polynomial K

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePolynomial p a b = (Polynomial.X ^ p - Polynomial.X) ^ 2 - Polynomial.C (4 * a * b)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePolynomial_eval {K : Type u_1} [Field K] (p : ℕ) (a b x : K) : Polynomial.eval x (harcosCurvePolynomial p a b) = (x ^ p - x) ^ 2 - 4 * a * b

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePolynomial_eval_zero {K : Type u_1} [Field K] (p : ℕ) (hp : 0 < p) (a b : K) : Polynomial.eval 0 (harcosCurvePolynomial p a b) = -(4 * a * b)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePolynomial_natDegree {K : Type u_1} [Field K] (p : ℕ) (hp : 1 < p) (a b : K) : (harcosCurvePolynomial p a b).natDegree = 2 * p

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePolynomial_eval_zero_ne {K : Type u_1} [Field K] (p : ℕ) (hp : 0 < p) (htwo : 2 ≠ 0) (a b : K) (ha : a ≠ 0) (hb : b ≠ 0) : Polynomial.eval 0 (harcosCurvePolynomial p a b) ≠ 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePolynomial_not_isSquare {K : Type u_1} [Field K] (p : ℕ) (hp : 1 < p) (htwo : 2 ≠ 0) (a b : K) (ha : a ≠ 0) (hb : b ≠ 0) : ¬IsSquare (harcosCurvePolynomial p a b)

The source's two factors have degree zero, contradicting their X^p coefficients: their sum has coefficient 2, which is nonzero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePolynomial_geometrically_not_isSquare {K : Type u_1} [Field K] (p : ℕ) (hp : 1 < p) (htwo : 2 ≠ 0) (a b : K) (ha : a ≠ 0) (hb : b ≠ 0) : ¬IsSquare (Polynomial.map (algebraMap K (AlgebraicClosure K)) (harcosCurvePolynomial p a b))

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePointCount {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : ℕ) (a b : F) : ℕ

The actual affine count in the last paragraph of Harcos, page 12.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePointCount p a b = {xy : F × F | xy.2 ^ 2 = (xy.1 ^ p - xy.1) ^ 2 - 4 * a * b}.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePointCount_eq_stepanovPointCount {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : ℕ) (a b : F) : harcosCurvePointCount p a b = stepanovPointCount (harcosCurvePolynomial p a b)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_curve_pointCount_bound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : ℕ) [CharP F p] (hp : Nat.Prime p) (hp2 : p ≠ 2) (a b : F) (ha : a ≠ 0) (hb : b ≠ 0) (hq : 12 * p < Fintype.card F) : |↑(harcosCurvePointCount p a b) - ↑(Fintype.card F)| < 8 * ↑p * ↑⌈√↑(Fintype.card F)⌉₊

Harcos's specialization, with all polynomial hypotheses discharged.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_twelve_mul_lt_pow (p n : ℕ) (hp : 3 ≤ p) (hn : 4 ≤ n) : 12 * p < p ^ n

The source's n ≥ 4 range is inside the range q > 12p.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_curve_pointCount_bound_of_card_eq_pow {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p n : ℕ) [CharP F p] (hp : Nat.Prime p) (hp2 : p ≠ 2) (a b : F) (ha : a ≠ 0) (hb : b ≠ 0) (hcard : Fintype.card F = p ^ n) (hn : 4 ≤ n) : |↑(harcosCurvePointCount p a b) - ↑p ^ n| < 8 * ↑p * ↑⌈√(↑p ^ n)⌉₊

In characteristic p, every finite field of size p^n, n ≥ 4, satisfies the specialized estimate, with no assumed curve bound.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_isSquare_taylor_iff {K : Type u_1} [Field K] (f : Polynomial K) (r : K) : IsSquare ((Polynomial.taylor r) f) ↔ IsSquare f

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_geometrically_not_isSquare_taylor_iff {K : Type u_1} [Field K] (f : Polynomial K) (r : K) : ¬IsSquare (Polynomial.map (algebraMap K (AlgebraicClosure K)) ((Polynomial.taylor r) f)) ↔ ¬IsSquare (Polynomial.map (algebraMap K (AlgebraicClosure K)) f)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovPointCount_taylor {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (f : Polynomial F) (r : F) : stepanovPointCount ((Polynomial.taylor r) f) = stepanovPointCount f

Translation is a bijection on the actual affine point sets.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_pointCount_bound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (f : Polynomial F) (hq : Odd (Fintype.card F)) (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 (pages/harcos-stepanov-08.png), without an f(0) ≠ 0 hypothesis. A nonroot exists since deg f < q, and translation preserves the degree, geometric nonsquareness, and affine point count.