Character-sum lemmas over a finite field

Elementary orthogonality relations for multiplicative characters and shared additive-character/Gauss-sum facts over a finite field K with values in ℂ. These are used by the phase-to-root-count identity and the MCM Fourier/phase development.

The multiplicative-character orthogonality section is characteristic independent. The shared additive-character section supplies the principal Gauss sum, characteristic-two self-inverse and Gauss-product identities, and related nonvanishing facts. Primitive-character nontriviality is supplied by Phase/AdditiveCharacter.lean.

@[instance_reducible]

noncomputable instance KasamiCyclicAdditive.Phase.instFintypeMulCharComplex (K : Type u_1) [Field K] [Fintype K] : Fintype (MulChar K ℂ)

The ℂ-valued multiplicative characters of a finite field form a finite type.

Equations

• KasamiCyclicAdditive.Phase.instFintypeMulCharComplex K = Fintype.ofFinite (MulChar K ℂ)

theorem KasamiCyclicAdditive.Phase.card_mulChar {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] : Fintype.card (MulChar K ℂ) = Fintype.card Kˣ

The number of ℂ-valued multiplicative characters of K is #Kˣ.

theorem KasamiCyclicAdditive.Phase.sum_char_apply {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (a : Kˣ) : ∑ χ : MulChar K ℂ, χ ↑a = if a = 1 then ↑(Fintype.card Kˣ) else 0

First orthogonality relation: summing the value at a fixed unit over all characters.

theorem KasamiCyclicAdditive.Phase.sum_units_char {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (θ : MulChar K ℂ) : ∑ b : Kˣ, θ ↑b = if θ = 1 then ↑(Fintype.card Kˣ) else 0

Second orthogonality relation: summing a fixed character over all units.

theorem KasamiCyclicAdditive.Phase.sum_cubic_char_apply {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (a : Kˣ) : ∑ χ : MulChar K ℂ with χ ^ 3 = 1, χ ↑a = ↑{b : Kˣ | b ^ 3 = a}.card

The sum of χ a over the cubic characters χ (those with χ ^ 3 = 1) equals the number of cube roots of a in Kˣ. This packages both the vanishing at non-cubes and the count at cubes into a single identity, and needs only the two orthogonality relations.

theorem KasamiCyclicAdditive.addChar_inv_self {K : Type u_1} [Field K] [CharP K 2] (psi : AddChar K ℂ) : psi⁻¹ = psi

In characteristic two an additive character is its own inverse.

theorem KasamiCyclicAdditive.sum_addChar_eq_zero {K : Type u_1} [Field K] [Fintype K] {psi : AddChar K ℂ} (hpsi : psi.IsPrimitive) (a : Kˣ) : ∑ x : K, psi (↑a * x) = 0

A primitive additive character sums to zero over K after any nonzero rescaling.

theorem KasamiCyclicAdditive.sum_units_addChar {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {psi : AddChar K ℂ} (hpsi : psi.IsPrimitive) (a : Kˣ) : ∑ x : Kˣ, psi (↑a * ↑x) = -1

Removing the term at 0, the same sum over Kˣ is -1.

theorem KasamiCyclicAdditive.gaussSum_principal {K : Type u_1} [Field K] [Fintype K] {psi : AddChar K ℂ} (hpsi : psi.IsPrimitive) : gaussSum 1 psi = -1

The Gauss sum of the principal character is -1.

theorem KasamiCyclicAdditive.gaussSum_mul_inv {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {psi : AddChar K ℂ} (hpsi : psi.IsPrimitive) {theta : MulChar K ℂ} (h : theta ≠ 1) : gaussSum theta psi * gaussSum theta⁻¹ psi = ↑(Fintype.card K)

In characteristic two, G(θ) G(θ⁻¹) = |K| for nonprincipal θ.

theorem KasamiCyclicAdditive.gaussSum_ne_zero_of_primitive {K : Type u_1} [Field K] [Fintype K] {psi : AddChar K ℂ} (hpsi : psi.IsPrimitive) (chi : MulChar K ℂ) : gaussSum chi psi ≠ 0

Against a primitive additive character no Gauss sum vanishes, principal character included.