Objects of the phase-to-root-count identity

Throughout, K is a finite field (in the application K = GF(2^n)), ψ is a primitive additive character of K with values in ℂ (in the application ψ x = (-1)^(Tr x)), and D is an exponent inverse to m modulo N = #Kˣ.

def KasamiCyclicAdditive.Phase.cubeRootsOne (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] : Finset K

U = μ₃(K), the group of cube roots of unity of K, as a finset.

Equations

• KasamiCyclicAdditive.Phase.cubeRootsOne K = {u : K | u ^ 3 = 1}

def KasamiCyclicAdditive.Phase.mu3Card (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] : ℕ

c = |μ₃(K)|.

Equations

• KasamiCyclicAdditive.Phase.mu3Card K = (KasamiCyclicAdditive.Phase.cubeRootsOne K).card

noncomputable def KasamiCyclicAdditive.Phase.phi {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (ψ : AddChar K ℂ) (D : ℕ) (x : K) : ℂ

Φ(x) = ∑_{u ∈ U} ψ(u x^D).

Equations

• KasamiCyclicAdditive.Phase.phi ψ D x = ∑ u ∈ KasamiCyclicAdditive.Phase.cubeRootsOne K, ψ (u * x ^ D)

noncomputable def KasamiCyclicAdditive.Phase.phiHat {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (ψ : AddChar K ℂ) (D : ℕ) (z : K) : ℂ

The additive Fourier transform Φ̂(z) = ∑_{t ∈ K} Φ(t) ψ(z t).

Equations

• KasamiCyclicAdditive.Phase.phiHat ψ D z = ∑ t : K, KasamiCyclicAdditive.Phase.phi ψ D t * ψ (z * t)

noncomputable def KasamiCyclicAdditive.Phase.weilSum {K : Type u_1} [Field K] [Fintype K] (ψ : AddChar K ℂ) (D : ℕ) (A B u v : K) : ℂ

W_{u,v} = ∑_{x,y ∈ K} ψ(u x^D + v (A x + B y)^D + y^D).

Equations

• KasamiCyclicAdditive.Phase.weilSum ψ D A B u v = ∑ x : K, ∑ y : K, ψ (u * x ^ D + v * (A * x + B * y) ^ D + y ^ D)

def KasamiCyclicAdditive.Phase.rootCount {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (D : ℕ) (A B u v : K) : ℕ

R_{u,v}(A,B) = #{t ∈ K : u t^D + v (A t + B)^D = 1}.

Equations

• KasamiCyclicAdditive.Phase.rootCount D A B u v = {t : K | u * t ^ D + v * (A * t + B) ^ D = 1}.card

noncomputable def KasamiCyclicAdditive.Phase.phaseTripleSum {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (S : K → ℂ) (rho sigma : K) : ℂ

Z(ρ) = ∑_{λ ∈ G} S(λ) S(ρ λ) S(σ λ).

Equations

• KasamiCyclicAdditive.Phase.phaseTripleSum S rho sigma = ∑ lam : Kˣ, S ↑lam * S (rho * ↑lam) * S (sigma * ↑lam)

def KasamiCyclicAdditive.Phase.WalshCharacterFormula {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (ψ : AddChar K ℂ) (e : ℕ) (S : K → ℂ) : Prop

The all-character Walsh formula 2 S(a) = (Q/N) ∑_χ [G(χ^e)/G(χ^3)] χ(a) for every a ∈ Kˣ, stated as a property of S rather than assumed.

Equations

• KasamiCyclicAdditive.Phase.WalshCharacterFormula ψ e S = ∀ (a : Kˣ), 2 * S ↑a = ↑(Fintype.card K) / ↑(Fintype.card Kˣ) * ∑ χ : MulChar K ℂ, gaussSum (χ ^ e) ψ / gaussSum (χ ^ 3) ψ * χ ↑a