Basic.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

The polynomial multiplication tensor

The coefficient tensor convolution a b represents multiplication of binary forms of degrees a - 1 and b - 1, or equivalently ordinary coefficient convolution. The output leg has a + b - 1 coordinates. The definitions also make sense when an input dimension is zero, while the nonzero and full-output-support statements use the positive dimensions assumed in Section 5 of the paper.

def OAI.MatrixMultiplication.AuxiliarySeparation.convolution line 24
Source documentation
The tensor C(a,b) of Section 5, in monomial coefficient coordinates.
```
def convolution (a b : ℕ) : Tensor ℂ (Fin a) (Fin b) (Fin (a + b - 1)) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_apply line 27
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_ne_zero_iff line 31
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_eq_one_iff line 37
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_eq_zero_iff line 43
def OAI.MatrixMultiplication.AuxiliarySeparation.convolutionOutput line 50
Source documentation
Every pair of input monomials has a valid output coordinate.
```
def convolutionOutput {a b : ℕ} (i : Fin a) (j : Fin b) : Fin (a + b - 1) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_at_output line 53
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_output_supported line 58
Source documentation
Every output monomial of the expected degree occurs in the product.
```
theorem convolution_output_supported {a b : ℕ} (ha : 0 < a) (hb : 0 < b)
    (k : Fin (a + b - 1)) :
    ∃ (i : Fin a) (j : Fin b), convolution a b i j k = 1 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_nonzero line 69
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_nonzero_iff line 79
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_comm line 100
Source documentation
Commuting the two inputs only casts the equal output dimensions.
```
theorem convolution_comm (a b : ℕ) (i : Fin a) (j : Fin b)
    (k : Fin (a + b - 1)) :
    convolution a b i j k =
      convolution b a j i (Fin.cast (by omega) k) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution, OAI.MatrixMultiplication.AuxiliarySeparation.omega
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_one_left line 107
Source documentation
The boundary tensor C(1,b) has the coefficient matrix of a dot product.
```
theorem convolution_one_left (b : ℕ) (i : Fin 1) (j : Fin b)
    (k : Fin (1 + b - 1)) :
    convolution 1 b i j k = if j.val = k.val then 1 else 0 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_one_right line 113
Source documentation
The other boundary tensor has the same coordinate identity.
```
theorem convolution_one_right (a : ℕ) (i : Fin a) (j : Fin 1)
    (k : Fin (a + 1 - 1)) :
    convolution a 1 i j k = if i.val = k.val then 1 else 0 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
def OAI.MatrixMultiplication.AuxiliarySeparation.convolutionOneOutputEquiv line 119
Source documentation
Relabel the output of C(1,b) by its actual dimension b.
```
def convolutionOneOutputEquiv (b : ℕ) : Fin b ≃ Fin (1 + b - 1) :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.convolutionOneInputEquiv line 123
Source documentation
Relabel the single input coordinate of C(1,b) by Unit.
```
def convolutionOneInputEquiv : Unit ≃ Fin 1 where
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_one_left_dotPairing line 130
Source documentation
C(1,b) is the dot-product tensor with the singleton on the first leg.
```
theorem convolution_one_left_dotPairing (b : ℕ) :
    Tensor.pullback convolutionOneInputEquiv (Equiv.refl (Fin b))
      (convolutionOneOutputEquiv b) (convolution 1 b) =
      Tensor.cyclic (Tensor.cyclic (Tensor.dotPairing (K := ℂ) (Fin b))) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolutionOneInputEquiv, OAI.MatrixMultiplication.AuxiliarySeparation.convolutionOneOutputEquiv, OAI.MatrixMultiplication.AuxiliarySeparation.convolution
def OAI.MatrixMultiplication.AuxiliarySeparation.convolutionRightOneOutputEquiv line 139
Source documentation
Relabel the output of C(a,1) by its actual dimension a.
```
def convolutionRightOneOutputEquiv (a : ℕ) : Fin a ≃ Fin (a + 1 - 1) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.convolution_one_right_dotPairing line 143
Source documentation
C(a,1) is the dot-product tensor with the singleton on the second leg.
```
theorem convolution_one_right_dotPairing (a : ℕ) :
    Tensor.pullback (Equiv.refl (Fin a)) convolutionOneInputEquiv
      (convolutionRightOneOutputEquiv a) (convolution a 1) =
      Tensor.cyclic (Tensor.dotPairing (K := ℂ) (Fin a)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolutionOneInputEquiv, OAI.MatrixMultiplication.AuxiliarySeparation.convolutionRightOneOutputEquiv, OAI.MatrixMultiplication.AuxiliarySeparation.convolution

theorem OAI.MatrixMultiplication.AuxiliarySeparation.contract_convolution line 152

Source documentation

Contracting the coefficient tensor computes ordinary finite convolution.

theorem contract_convolution {a b : ℕ} (x : Fin a → ℂ) (y : Fin b → ℂ)
    (k : Fin (a + b - 1)) :
    Tensor.contract (convolution a b) x y k =
      ∑ i : Fin a, ∑ j : Fin b,
        if i.val + j.val = k.val then x i * y j else 0 := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution