RankLowerBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact rank of polynomial convolution

Each output coefficient of polynomial multiplication occurs in some product of two input monomials. Choosing one such pair for each output gives an identity minor in the output flattening. Together with evaluation and interpolation, this proves the exact rank of C(a,b) for positive dimensions.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_identity_minor line 23
Source documentation
Choosing one product for every output monomial gives an identity minor of the output flattening.
```
theorem convolution_identity_minor {a b : ℕ} (ha : 0 < a) (hb : 0 < b) :
    ∃ (x : Fin (a + b - 1) → Fin a) (y : Fin (a + b - 1) → Fin b),
      ∀ k l, convolution a b (x k) (y k) l = if k = l then 1 else 0 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_rank_lower line 35
Source documentation
Every rank decomposition of convolution has at least one term per output coefficient.
```
theorem convolution_rank_lower {a b r : ℕ} (ha : 0 < a) (hb : 0 < b)
    (hRank : Tensor.RankAtMost (convolution a b) r) : a + b - 1 ≤ r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRank_convolution line 42
Source documentation
Polynomial multiplication has exact rank a+b-1 when both inputs have positive dimension.
```
theorem exactRank_convolution {a b : ℕ} (ha : 0 < a) (hb : 0 < b) :
    exactRank (convolution a b) = a + b - 1 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRank, OAI.MatrixMultiplication.AuxiliarySeparation.convolution