Quadratic character sums and conic points

Evaluate quadratic character sums and use them to find conic points avoiding a prescribed small exceptional set.

theorem BGS.FiniteField.sum_comp_sq_eq_sum_quadraticChar_add_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (f : F → ℤ) : ∑ y : F, f (y ^ 2) = ∑ x : F, ((quadraticChar F) x + 1) * f x

Sum a function over the square map, with fiber sizes expressed by the quadratic character.

theorem BGS.FiniteField.sum_quadraticChar_one_sub_mul_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {d : F} (hd : d ≠ 0) : ∑ y : F, (quadraticChar F) (1 - d * y ^ 2) = -(quadraticChar F) d * (quadraticChar F) (-1)

The quadratic-character sum of 1 - d * y² is a Jacobi sum.

theorem BGS.FiniteField.sum_quadraticChar_mul_sq_sub {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {A C : F} (hA : A ≠ 0) (hC : C ≠ 0) : ∑ y : F, (quadraticChar F) (A * y ^ 2 - C) = -(quadraticChar F) A

A nondegenerate quadratic polynomial has quadratic-character sum -chi(A).

theorem BGS.FiniteField.exists_quadratic_conic_point_away_from_three {F : Type u_1} [Field F] [Fintype F] (hF : ringChar F ≠ 2) (hcard : 8 ≤ Fintype.card F) {A C : F} (hA : A ≠ 0) (hC : C ≠ 0) (bad : Finset F) (hbad : bad.card ≤ 3) : ∃ y ∉ bad, ∃ (lambda : F), lambda ^ 2 = A * y ^ 2 - C

A nondegenerate affine conic has a point outside any set of at most three forbidden first coordinates once the field has at least eight elements.