Finite coefficient tensors and their algebraic transformations.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients {K : Type u_1} [CommSemiring K] (A : Type u_8) (B : Type u_9) (C : Type u_10) [DecidableEq A] [DecidableEq B] [DecidableEq C] : Tensor K (A × B) (B × C) (C × A)

The coefficient tensor of matrix multiplication on arbitrary decidable coordinate sets.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients A B C x y z = if x.2 = y.1 ∧ y.2 = z.1 ∧ z.2 = x.1 then 1 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_eq_matrixCoefficients (a b c : ℕ) : matrixMultiplication a b c = matrixCoefficients (Fin a) (Fin b) (Fin c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.contract_matrixCoefficients {K : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring K] [Fintype A] [Fintype B] [Fintype C] [DecidableEq A] [DecidableEq B] [DecidableEq C] (left : A × B → K) (right : B × C → K) (i : A) (k : C) : (matrixCoefficients A B C).contract left right (k, i) = ∑ j : B, left (i, j) * right (j, k)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_product {K : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} {F : Type u_7} [CommSemiring K] [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D] [DecidableEq E] [DecidableEq F] (x : (A × D) × B × E) (y : (B × E) × C × F) (z : (C × F) × A × D) : (matrixCoefficients A B C).product (matrixCoefficients D E F) ((x.1.1, x.2.1), x.1.2, x.2.2) ((y.1.1, y.2.1), y.1.2, y.2.2) ((z.1.1, z.2.1), z.1.2, z.2.2) = matrixCoefficients (A × D) (B × E) (C × F) x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_cyclic {K : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring K] [DecidableEq A] [DecidableEq B] [DecidableEq C] (x : B × C) (y : C × A) (z : A × B) : matrixCoefficients A B C z x y = matrixCoefficients B C A x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_product {K : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} {F : Type u_7} [CommSemiring K] [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D] [DecidableEq E] [DecidableEq F] {r : ℕ} (hproduct : ((matrixCoefficients A B C).product (matrixCoefficients D E F)).RankAtMost r) : (matrixCoefficients (A × D) (B × E) (C × F)).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_product_rank {K : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} {F : Type u_7} [CommSemiring K] [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D] [DecidableEq E] [DecidableEq F] {r s : ℕ} (hT : (matrixCoefficients A B C).RankAtMost r) (hS : (matrixCoefficients D E F).RankAtMost s) : (matrixCoefficients (A × D) (B × E) (C × F)).RankAtMost (r * s)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_batch_rank {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [DecidableEq A] [DecidableEq B] [Finite B] {R k r batches : ℕ} (houter : (matrixCoefficients A A A).RankAtMost R) (hbatch : (directSum fun (x : Fin k) => matrixCoefficients B B B).RankAtMost r) (hfit : R ≤ batches * k) : (matrixCoefficients (A × B) (A × B) (A × B)).RankAtMost (batches * r)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_power {K : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring K] [DecidableEq A] [DecidableEq B] [DecidableEq C] (n : ℕ) (x : (Fin n → A) × (Fin n → B)) (y : (Fin n → B) × (Fin n → C)) (z : (Fin n → C) × (Fin n → A)) : ((matrixCoefficients A B C).power n (fun (i : Fin n) => (x.1 i, x.2 i)) (fun (i : Fin n) => (y.1 i, y.2 i)) fun (i : Fin n) => (z.1 i, z.2 i)) = matrixCoefficients (Fin n → A) (Fin n → B) (Fin n → C) x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_cyclic_rank {K : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring K] [DecidableEq A] [DecidableEq B] [DecidableEq C] {r : ℕ} (h : (matrixCoefficients A B C).RankAtMost r) : (matrixCoefficients B C A).RankAtMost r