Rank.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial convolution by evaluation and interpolation

Evaluating the two input polynomials at a + b - 1 distinct complex points, then interpolating their product, expresses the convolution tensor as a sum of a + b - 1 rank-one tensors. This is the polynomial multiplication rank upper bound used in Section 5.

lemma OAI.MatrixMultiplication.AuxiliarySeparation.monomial_coeff_eq_sum_interpolation line 23

Source documentation

Recover each monomial coefficient from evaluations at distinct nodes.

lemma monomial_coeff_eq_sum_interpolation {n m : ℕ} (hm : m < n)
    (v : Fin n → ℂ) (hv : Function.Injective v) (k : ℕ) :
    (if m = k then (1 : ℂ) else 0) =
      ∑ r : Fin n, v r ^ m * (Lagrange.basis Finset.univ v r).coeff k := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_eq_sum_rankOne line 37

Source documentation

Evaluation at distinct nodes and Lagrange interpolation give an explicit rank-one decomposition of polynomial convolution.

theorem convolution_eq_sum_rankOne {a b : ℕ}
    (v : Fin (a + b - 1) → ℂ) (hv : Function.Injective v) :
    convolution a b = fun i j k => ∑ r : Fin (a + b - 1),
      Tensor.rankOne (fun i : Fin a => v r ^ i.val)
        (fun j : Fin b => v r ^ j.val)
        (fun k : Fin (a + b - 1) => (Lagrange.basis Finset.univ v r).coeff k.val)
        i j k := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution

theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_rankAtMost line 50
Source documentation
The convolution tensor C(a,b) has rank at most a + b - 1 over ℂ.
```
theorem convolution_rankAtMost (a b : ℕ) :
    Tensor.RankAtMost (convolution a b) (a + b - 1) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_borderRankAtMost line 65
Source documentation
The interpolation algorithm also bounds border rank.
```
theorem convolution_borderRankAtMost (a b : ℕ) :
    Tensor.BorderRankAtMost (convolution a b) (a + b - 1) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution