Finite coefficient tensors and their algebraic transformations.
def
MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.diagonal
{K : Type u_1}
[CommSemiring K]
(ι : Type u_8)
[DecidableEq ι]
:
Tensor K ι ι ι
The diagonal tensor with coefficient one exactly when all three indices agree.
Equations
Instances For
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.diagonal_rankAtMost
{K : Type u_1}
[CommSemiring K]
(ι : Type u_8)
[Fintype ι]
[DecidableEq ι]
:
(diagonal ι).RankAtMost (Fintype.card ι)
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.repeat_batch
{K : Type u_1}
{U : Type u_5}
{V : Type u_6}
{W : Type u_7}
[CommSemiring K]
{S : Tensor K U V W}
{k r R B : ℕ}
(hbatch : (directSum fun (x : Fin k) => S).RankAtMost r)
(hfit : R ≤ B * k)
:
(directSum fun (x : Fin R) => S).RankAtMost (B * r)
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.batch_substitute
{K : Type u_1}
{X : Type u_2}
{Y : Type u_3}
{Z : Type u_4}
{U : Type u_5}
{V : Type u_6}
{W : Type u_7}
[CommSemiring K]
[Finite U]
[Finite V]
[Finite W]
{T : Tensor K X Y Z}
{S : Tensor K U V W}
{r b : ℕ}
(hT : T.RankAtMost r)
(hbatch : (directSum fun (x : Fin r) => S).RankAtMost b)
:
(T.product S).RankAtMost b
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.batch_product
{K : Type u_1}
{X : Type u_2}
{Y : Type u_3}
{Z : Type u_4}
{U : Type u_5}
{V : Type u_6}
{W : Type u_7}
[CommSemiring K]
[Finite U]
[Finite V]
[Finite W]
{T : Tensor K X Y Z}
{S : Tensor K U V W}
{R k r B : ℕ}
(hT : T.RankAtMost R)
(hbatch : (directSum fun (x : Fin k) => S).RankAtMost r)
(hfit : R ≤ B * k)
:
(T.product S).RankAtMost (B * r)