Sums over a finite field weighted by the quadratic character

Let F be a finite field of odd characteristic with quadratic character χ. For a ≠ 0, the value u = a t² has 1 + χ(a u) preimages t, by Mathlib's quadraticChar_card_sqrts. Hence a sum over t of a function of a t² is a sum over u weighted by 1 + χ(a u). Similarly the quadratic character sums to zero against any nonzero dilation, and the quadratic Jacobi sum ∑ᵤ χ(u (c - u)) is evaluated through Mathlib's jacobiSum_nontrivial_inv.

Main results

• TauCeti.sum_comp_mul_sq: ∑ₜ g(a t²) = ∑ᵤ (1 + χ(a u)) • g(u) for a ≠ 0.
• TauCeti.sum_quadraticChar_mul: ∑ᵤ χ(a u) = 0 for a ≠ 0.
• TauCeti.sum_quadraticChar_mul_sub: the quadratic Jacobi sum ∑ᵤ χ(u (c - u)).

theorem TauCeti.sum_comp_mul_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {M : Type u_2} [AddCommGroup M] (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) (g : F → M) : ∑ t : F, g (a * t ^ 2) = ∑ u : F, (1 + (quadraticChar F) (a * u)) • g u

Grouping a sum by squares: for a ≠ 0 in a finite field of odd characteristic, the value u = a t² has 1 + χ(a u) preimages t, so ∑ₜ g(a t²) = ∑ᵤ (1 + χ(a u)) • g(u).

theorem TauCeti.sum_quadraticChar_mul {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) : ∑ u : F, (quadraticChar F) (a * u) = 0

The quadratic character sums to zero against any nonzero dilation.

theorem TauCeti.sum_quadraticChar_mul_sub {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (c : F) : ∑ u : F, (quadraticChar F) (u * (c - u)) = (quadraticChar F) (-1) * if c = 0 then ↑(Fintype.card F) - 1 else -1

The quadratic Jacobi sum: in a finite field of odd characteristic, ∑ᵤ χ(u (c - u)) is χ(-1) (q - 1) for c = 0 and -χ(-1) otherwise.