Character sums over linear codes

Let ψ be a primitive additive character of a finite commutative ring R, with values in a domain. For a linear code C ≤ ι → R, the character c ↦ ψ (c ⬝ᵥ y) of C is trivial exactly when y lies in the Euclidean dual of C, so

∑ c ∈ C, ψ (c ⬝ᵥ y) = if y ∈ C⊥ then #C else 0.

Summing this orthogonality relation against an arbitrary function f on words gives the Poisson summation formula for the finite Fourier transform f̂ x = ∑ y, ψ (x ⬝ᵥ y) • f y:

∑ c ∈ C, f̂ c = #C • ∑ y ∈ C⊥, f y.

This is the analytic input of the MacWilliams identity; it is stated for an arbitrary f with values in a module over the target of ψ so that it applies to polynomial-valued weight monomials. Every finite field carries a primitive character with values in a field of characteristic zero (AddChar.FiniteField.primitiveChar), and so does every ZMod m (AddChar.primitiveZModChar).

Main statements

• Submodule.sum_addChar_dotProduct: the orthogonality relation for a code and its dual.
• Submodule.sum_sum_addChar_dotProduct_smul: the Poisson summation formula.
• AddChar.sum_apply_dotProduct: the orthogonality relation for the full space ι → R.

References

F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland (1977), Chapter 5, §2, Lemmas 2 and 11; W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press (2003), §7.2.

theorem Submodule.sum_addChar_dotProduct {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype ι] [CommRing R] [CommRing S] [IsDomain S] {ψ : AddChar R S} {C : Submodule R (ι → R)} [Fintype ↥C] [DecidablePred fun (x : ι → R) => x ∈ C.euclideanDual] (hψ : ψ.IsPrimitive) (y : ι → R) : ∑ c : ↥C, ψ (↑c ⬝ᵥ y) = if y ∈ C.euclideanDual then ↑(Fintype.card ↥C) else 0

The orthogonality relation for a linear code and its Euclidean dual: summing a primitive additive character over the values c ⬝ᵥ y, c ∈ C, gives #C when y is dual to C and zero otherwise.

theorem Submodule.sum_sum_addChar_dotProduct_smul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype ι] [CommRing R] [CommRing S] [IsDomain S] {ψ : AddChar R S} {C : Submodule R (ι → R)} [DecidableEq ι] [Fintype R] [Fintype ↥C] [Fintype ↥C.euclideanDual] {M : Type u_4} [AddCommMonoid M] [Module S M] (hψ : ψ.IsPrimitive) (f : (ι → R) → M) : ∑ c : ↥C, ∑ y : ι → R, ψ (↑c ⬝ᵥ y) • f y = Fintype.card ↥C • ∑ y : ↥C.euclideanDual, f ↑y

The Poisson summation formula for a linear code: the finite Fourier transform f̂ x = ∑ y, ψ (x ⬝ᵥ y) • f y of a function on words, summed over the code C, is #C times the sum of f over the Euclidean dual of C.

theorem AddChar.sum_apply_dotProduct {ι : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [Fintype R] [DecidableEq R] [CommRing S] [IsDomain S] {ψ : AddChar R S} (hψ : ψ.IsPrimitive) (v : ι → R) : ∑ z : ι → R, ψ (v ⬝ᵥ z) = if v = 0 then ↑(Fintype.card R) ^ Fintype.card ι else 0

The orthogonality relation for the full space ι → R: summing a primitive additive character over the values v ⬝ᵥ z, z : ι → R, gives #R ^ #ι when v = 0 and zero otherwise. This is the case of the full code in Submodule.sum_addChar_dotProduct.