Finite root-of-unity filters

Averaging the integer powers of a primitive root over one period detects exactly the exponents divisible by that period. This is the finite Fourier filter used for auxiliary separation.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sum_pow_root_of_unity {K : Type} [Field K] (z : K) (L : ℕ) (hz : z ^ L = 1) : ∑ r ∈ Finset.range L, z ^ r = if z = 1 then ↑L else 0

The sum over a complete period of a root of unity is zero unless the root is one.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sum_zpow_primitive_root {K : Type} [Field K] {ζ : K} {L : ℕ} (hζ : IsPrimitiveRoot ζ L) (e : ℤ) : ∑ r ∈ Finset.range L, ζ ^ (↑r * e) = if ↑L ∣ e then ↑L else 0

An unnormalized finite Fourier filter, with an integer exponent.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalized_sum_zpow_primitive_root {K : Type} [Field K] {ζ : K} {L : ℕ} (hL : ↑L ≠ 0) (hζ : IsPrimitiveRoot ζ L) (e : ℤ) : (↑L)⁻¹ * ∑ r ∈ Finset.range L, ζ ^ (↑r * e) = if ↑L ∣ e then 1 else 0

Averaging over a primitive root's period selects exactly its divisible exponents.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.int_dvd_iff_eq_zero_of_abs_lt {L : ℕ} {e : ℤ} (he : |e| < ↑L) : ↑L ∣ e ↔ e = 0

Divisibility by a positive period is exact equality to zero inside one period.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.normalized_sum_zpow_primitive_root_of_abs_lt {K : Type} [Field K] {ζ : K} {L : ℕ} {e : ℤ} (hL : ↑L ≠ 0) (hζ : IsPrimitiveRoot ζ L) (he : |e| < ↑L) : (↑L)⁻¹ * ∑ r ∈ Finset.range L, ζ ^ (↑r * e) = if e = 0 then 1 else 0

Within one period, the finite Fourier filter selects exactly exponent zero.