OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Separation/FiniteProjection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exact finite Fourier projection and square filtering

The 5 * M-term Fourier average 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.

  1. def OAI.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient line 26

    Source documentation

    A normalized finite Fourier average of one branch coefficient.

    noncomputable def finiteFourierCoefficient (ζ : ℂ) (L : ℕ) (e : ℤ) (c : ℂ) : ℂ :=
…
  2. theorem OAI.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient_eq_ite line 30

    Source documentation

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

    theorem finiteFourierCoefficient_eq_ite {ζ : ℂ} {L : ℕ}
    (hL : L ≠ 0) (hζ : IsPrimitiveRoot ζ L) (e : ℤ) (c : ℂ) :
    finiteFourierCoefficient ζ L e c = if (L : ℤ) ∣ e then c else 0 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient

  3. theorem OAI.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient_sum line 38

    Source documentation

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

    theorem finiteFourierCoefficient_sum {ι : Type*} (s : Finset ι)
    (ζ : ℂ) (L : ℕ) (e : ι → ℤ) (c : ι → ℂ) :
    (L : ℂ)⁻¹ * (∑ r ∈ Finset.range L, ∑ i ∈ s, ζ ^ ((r : ℤ) * e i) * c i) =
      ∑ i ∈ s, finiteFourierCoefficient ζ L (e i) (c i) := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient

  4. theorem OAI.MatrixMultiplication.AuxiliarySeparation.fiveMFourierCoefficient_eq_ite line 46

    Source documentation

    Exactly 5 * M phases select the integer support equation.

    theorem fiveMFourierCoefficient_eq_ite {ζ : ℂ} {M : ℕ} {g h u v : ℤ}
    (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (hg : 1 ≤ g ∧ g ≤ M) (hh : 1 ≤ h ∧ h ≤ M)
    (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) (c : ℂ) :
    finiteFourierCoefficient ζ (5 * M) (phase g h u v) c =
      if phase g h u v = 0 then c else 0 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.finiteFourierCoefficient, OAI.MatrixMultiplication.AuxiliarySeparation.phase

  5. def OAI.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial line 59

    Source documentation

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

    noncomputable def projectedBranchPolynomial (ζ : ℂ) (M : ℕ)
    (g h u v : ℤ) (c : ℂ) : Polynomial ℂ :=
…
  6. theorem OAI.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial_eq_ite line 65

    Source documentation

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

    theorem projectedBranchPolynomial_eq_ite {ζ : ℂ} {M : ℕ} {g h u v : ℤ}
    (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (hg : 1 ≤ g ∧ g ≤ M) (hh : 1 ≤ h ∧ h ≤ M)
    (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) (c : ℂ) :
    projectedBranchPolynomial ζ M g h u v c =
      if phase g h u v = 0 then Polynomial.monomial ((g - h) ^ 2).toNat c else 0 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial, OAI.MatrixMultiplication.AuxiliarySeparation.phase

  7. theorem OAI.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial_coeff line 78

    Source documentation

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

    theorem projectedBranchPolynomial_coeff {ζ : ℂ} {M n : ℕ} {g h u v : ℤ}
    (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (hg : 1 ≤ g ∧ g ≤ M) (hh : 1 ≤ h ∧ h ≤ M)
    (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) (c : ℂ) :
    (projectedBranchPolynomial ζ M g h u v c).coeff n =
      if phase g h u v = 0 ∧ totalWeight g h u v = (n : ℤ) then c else 0 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial, OAI.MatrixMultiplication.AuxiliarySeparation.phase, OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight

  8. theorem OAI.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial_coeff_eq_zero_of_lt line 94

    Source documentation

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

    theorem projectedBranchPolynomial_coeff_eq_zero_of_lt
    {ζ : ℂ} {M n : ℕ} {g h u v : ℤ}
    (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (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 : ℂ) :
    (projectedBranchPolynomial ζ M g h u v c).coeff n = 0 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial

  9. theorem OAI.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial_coeff_zero line 110

    Source documentation

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

    theorem projectedBranchPolynomial_coeff_zero {ζ : ℂ} {M : ℕ} {g h u v : ℤ}
    (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (hg : 1 ≤ g ∧ g ≤ M) (hh : 1 ≤ h ∧ h ≤ M)
    (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) (c : ℂ) :
    (projectedBranchPolynomial ζ M g h u v c).coeff 0 =
      if g = h ∧ u = v then c else 0 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.projectedBranchPolynomial

  10. def OAI.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial line 127

    Source documentation

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

    noncomputable def projectedPolynomial {ι : Type*} (s : Finset ι)
    (ζ : ℂ) (M : ℕ) (g h u v : ι → ℤ) (c : ι → ℂ) : Polynomial ℂ :=
…
  11. theorem OAI.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial_coeff line 132

    Source documentation

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

    theorem projectedPolynomial_coeff {ι : Type*} (s : Finset ι)
    {ζ : ℂ} {M n : ℕ} (g h u v : ι → ℤ) (c : ι → ℂ)
    (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (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 ζ M 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 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial, OAI.MatrixMultiplication.AuxiliarySeparation.phase, OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight

  12. theorem OAI.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial_coeff_zero line 149

    Source documentation

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

    theorem projectedPolynomial_coeff_zero {ι : Type*} (s : Finset ι)
    {ζ : ℂ} {M : ℕ} (g h u v : ι → ℤ) (c : ι → ℂ)
    (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (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 ζ M g h u v c).coeff 0 =
      ∑ i ∈ s, if g i = h i ∧ u i = v i then c i else 0 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial

  13. theorem OAI.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial_coeff_eq_zero_of_lt line 165

    Source documentation

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

    theorem projectedPolynomial_coeff_eq_zero_of_lt {ι : Type*} (s : Finset ι)
    {ζ : ℂ} {M n : ℕ} (g h u v : ι → ℤ) (c : ι → ℂ)
    (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (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 ζ M g h u v c).coeff n = 0 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial

  14. theorem OAI.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial_natDegree_le line 181

    Source documentation

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

    theorem projectedPolynomial_natDegree_le {ι : Type*} (s : Finset ι)
    {ζ : ℂ} {M : ℕ} (g h u v : ι → ℤ) (c : ι → ℂ)
    (hM : 0 < M) (hζ : IsPrimitiveRoot ζ (5 * M))
    (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 ζ M g h u v c).natDegree ≤ (M - 1) ^ 2 := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.projectedPolynomial