Exact finite Fourier projection and square filtering

The L-term Fourier average (the paper: L = 5 * M) is applied to an arbitrary branch coefficient. The label bounds eliminate modular wrap. The weights on the three tensor legs then give a nonnegative square degree on every surviving branch. Taking the constant coefficient retains exactly the branches with g = h and u = v.

The finite-family statements permit arbitrary coefficients and arbitrary repetitions of labels; they use only linearity of the Fourier projection and coefficient extraction, without assumptions on an ambient tensor.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient {K : Type} [Field K] (ζ : K) (L : ℕ) (e : ℤ) (c : K) : K

A normalized finite Fourier average of one branch coefficient.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient ζ L e c = (↑L)⁻¹ * ∑ r ∈ Finset.range L, ζ ^ (↑r * e) * c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient_eq_ite {K : Type} [Field K] {ζ : K} {L : ℕ} (hL : ↑L ≠ 0) (hζ : IsPrimitiveRoot ζ L) (e : ℤ) (c : K) : finiteFourierCoefficient ζ L e c = if ↑L ∣ e then c else 0

The Fourier average is a scalar support indicator, for every coefficient.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient_sum {K : Type} [Field K] {ι : Type u_1} (s : Finset ι) (ζ : K) (L : ℕ) (e : ι → ℤ) (c : ι → K) : (↑L)⁻¹ * ∑ r ∈ Finset.range L, ∑ i ∈ s, ζ ^ (↑r * e i) * c i = ∑ i ∈ s, finiteFourierCoefficient ζ L (e i) (c i)

Averaging a finite family of branches agrees with averaging each branch.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fiveMFourierCoefficient_eq_ite {K : Type} [Field K] {ζ : K} {M L : ℕ} {g h u v : ℤ} (_hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (hg : 1 ≤ g ∧ g ≤ ↑M) (hh : 1 ≤ h ∧ h ≤ ↑M) (hu : 1 ≤ u ∧ u ≤ ↑M) (hv : 1 ≤ v ∧ v ≤ ↑M) (c : K) : finiteFourierCoefficient ζ L (phase g h u v) c = if phase g h u v = 0 then c else 0

Exactly L phases select the integer support equation, for any period L > 3 * (M - 1) that is nonzero in K (the paper uses L = 5 * M).

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial {K : Type} [Field K] (ζ : K) (L : ℕ) (g h u v : ℤ) (c : K) : Polynomial K

A projected branch, recorded as an ordinary polynomial after Fourier averaging.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial_eq_ite {K : Type} [Field K] {ζ : K} {M L : ℕ} {g h u v : ℤ} (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (hg : 1 ≤ g ∧ g ≤ ↑M) (hh : 1 ≤ h ∧ h ≤ ↑M) (hu : 1 ≤ u ∧ u ≤ ↑M) (hv : 1 ≤ v ∧ v ≤ ↑M) (c : K) : projectedBranchPolynomial ζ L g h u v c = if phase g h u v = 0 then (Polynomial.monomial ((g - h) ^ 2).toNat) c else 0

The surviving polynomial weight is the square (g - h)^2.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial_coeff {K : Type} [Field K] {ζ : K} {M L n : ℕ} {g h u v : ℤ} (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (hg : 1 ≤ g ∧ g ≤ ↑M) (hh : 1 ≤ h ∧ h ≤ ↑M) (hu : 1 ≤ u ∧ u ≤ ↑M) (hv : 1 ≤ v ∧ v ≤ ↑M) (c : K) : (projectedBranchPolynomial ζ L g h u v c).coeff n = if phase g h u v = 0 ∧ totalWeight g h u v = ↑n then c else 0

A coefficient occurs exactly on the Fourier support at its integer total weight.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial_coeff_eq_zero_of_lt {K : Type} [Field K] {ζ : K} {M L n : ℕ} {g h u v : ℤ} (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (hg : 1 ≤ g ∧ g ≤ ↑M) (hh : 1 ≤ h ∧ h ≤ ↑M) (hu : 1 ≤ u ∧ u ≤ ↑M) (hv : 1 ≤ v ∧ v ≤ ↑M) (hn : (M - 1) ^ 2 < n) (c : K) : (projectedBranchPolynomial ζ L g h u v c).coeff n = 0

Each projected branch has no polynomial coefficient above (M - 1)^2.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial_coeff_zero {K : Type} [Field K] {ζ : K} {M L : ℕ} {g h u v : ℤ} (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (hg : 1 ≤ g ∧ g ≤ ↑M) (hh : 1 ≤ h ∧ h ≤ ↑M) (hu : 1 ≤ u ∧ u ≤ ↑M) (hv : 1 ≤ v ∧ v ≤ ↑M) (c : K) : (projectedBranchPolynomial ζ L g h u v c).coeff 0 = if g = h ∧ u = v then c else 0

Constant coefficient extraction is the exact square filter, with no restriction on the original coefficient.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial {K : Type} [Field K] {ι : Type u_1} (s : Finset ι) (ζ : K) (L : ℕ) (g h u v : ι → ℤ) (c : ι → K) : Polynomial K

Apply the finite Fourier projection and square weights branch by branch.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial_coeff {K : Type} [Field K] {ι : Type u_1} (s : Finset ι) {ζ : K} {M L n : ℕ} (g h u v : ι → ℤ) (c : ι → K) (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (hg : ∀ i ∈ s, 1 ≤ g i ∧ g i ≤ ↑M) (hh : ∀ i ∈ s, 1 ≤ h i ∧ h i ≤ ↑M) (hu : ∀ i ∈ s, 1 ≤ u i ∧ u i ≤ ↑M) (hv : ∀ i ∈ s, 1 ≤ v i ∧ v i ≤ ↑M) : (projectedPolynomial s ζ L g h u v c).coeff n = ∑ i ∈ s, if phase (g i) (h i) (u i) (v i) = 0 ∧ totalWeight (g i) (h i) (u i) (v i) = ↑n then c i else 0

Every coefficient of the projected polynomial has the exact integer support.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial_coeff_zero {K : Type} [Field K] {ι : Type u_1} (s : Finset ι) {ζ : K} {M L : ℕ} (g h u v : ι → ℤ) (c : ι → K) (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (hg : ∀ i ∈ s, 1 ≤ g i ∧ g i ≤ ↑M) (hh : ∀ i ∈ s, 1 ≤ h i ∧ h i ≤ ↑M) (hu : ∀ i ∈ s, 1 ≤ u i ∧ u i ≤ ↑M) (hv : ∀ i ∈ s, 1 ≤ v i ∧ v i ≤ ↑M) : (projectedPolynomial s ζ L g h u v c).coeff 0 = ∑ i ∈ s, if g i = h i ∧ u i = v i then c i else 0

Exact finite filtering for an arbitrary finite family of branch coefficients.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial_coeff_eq_zero_of_lt {K : Type} [Field K] {ι : Type u_1} (s : Finset ι) {ζ : K} {M L n : ℕ} (g h u v : ι → ℤ) (c : ι → K) (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (hg : ∀ i ∈ s, 1 ≤ g i ∧ g i ≤ ↑M) (hh : ∀ i ∈ s, 1 ≤ h i ∧ h i ≤ ↑M) (hu : ∀ i ∈ s, 1 ≤ u i ∧ u i ≤ ↑M) (hv : ∀ i ∈ s, 1 ≤ v i ∧ v i ≤ ↑M) (hn : (M - 1) ^ 2 < n) : (projectedPolynomial s ζ L g h u v c).coeff n = 0

The finite projected polynomial has support only in degrees at most (M - 1)^2.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial_natDegree_le {K : Type} [Field K] {ι : Type u_1} (s : Finset ι) {ζ : K} {M L : ℕ} (g h u v : ι → ℤ) (c : ι → K) (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (hg : ∀ i ∈ s, 1 ≤ g i ∧ g i ≤ ↑M) (hh : ∀ i ∈ s, 1 ≤ h i ∧ h i ≤ ↑M) (hu : ∀ i ∈ s, 1 ≤ u i ∧ u i ≤ ↑M) (hv : ∀ i ∈ s, 1 ≤ v i ∧ v i ≤ ↑M) : (projectedPolynomial s ζ L g h u v c).natDegree ≤ (M - 1) ^ 2

The degree bound is independent of the number or values of the coefficients.