Dot.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Dot-product exponents of tensor characters

The power laws here follow from restriction monotonicity and tensor products. They are not additional assumptions on a character. The three exponents refer to the leg on which the corresponding dot product has dimension one.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_pos line 24
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.cyclicCharacter line 29
Source documentation
Precomposing a character with a cyclic permutation gives a character.
```
def cyclicCharacter : Character where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.cyclicCharacter_value line 54
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.dotPairing_ne_zero line 58
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.dotPairing_rank line 64
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing_pos line 74
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing_le line 78
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing_mono line 82
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing_mul line 92
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.pZ line 107
Source documentation
The exponent on dot products whose third leg has dimension one.
```
def pZ : ℝ :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.pY line 111
Source documentation
The exponent on dot products whose second leg has dimension one.
```
def pY : ℝ := χ.cyclicCharacter.pZ
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.pX line 114
Source documentation
The exponent on dot products whose first leg has dimension one.
```
def pX : ℝ := χ.cyclicCharacter.cyclicCharacter.pZ
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.pZ_nonneg line 116
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.pZ_le_one line 120
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.pY_nonneg line 124
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.pY_le_one line 125
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.pX_nonneg line 126
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.pX_le_one line 127
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing line 129
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_cyclic_dotPairing line 137
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_cyclic_cyclic_dotPairing line 142
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_matrixCoefficients line 148
Source documentation
Exact factorization through the three oriented dot products.
```
theorem value_matrixCoefficients {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    χ.value (Tensor.matrixCoefficients (K := ℂ) (Fin a) (Fin b) (Fin c)) =
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_matrixCoefficients_square line 156
Source documentation
The character of square matrix multiplication has exponent pX + pY + pZ.
```
theorem value_matrixCoefficients_square {m : ℕ} (hm : 0 < m) :
    χ.value (Tensor.matrixCoefficients (K := ℂ) (Fin m) (Fin m) (Fin m)) =
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_matrixMultiplication line 165
Source documentation
The same power law in the matrix-tensor notation used for exact rank.
```
theorem value_matrixMultiplication {m : ℕ} (hm : 0 < m) :
    χ.value (Tensor.matrixMultiplication m m m) =
      (m : ℝ) ^ (χ.pX + χ.pY + χ.pZ) := by
…
```