Rectangular matrix multiplication algorithms and their asymptotic exponents.
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Tensor.rectangular_rank_of_injective
{K : Type u_1}
{A : Type u_2}
{B : Type u_3}
{C : Type u_4}
{A' : Type u_5}
{B' : Type u_6}
{C' : Type u_7}
[CommSemiring K]
[DecidableEq A]
[DecidableEq B]
[DecidableEq C]
[DecidableEq A']
[DecidableEq B']
[DecidableEq C']
{R : ℕ}
(h : (Foundation.Tensor.matrixCoefficients A B C).RankAtMost R)
(f : A' → A)
(hf : Function.Injective f)
(g : B' → B)
(hg : Function.Injective g)
(j : C' → C)
(hj : Function.Injective j)
:
(Foundation.Tensor.matrixCoefficients A' B' C').RankAtMost R
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Tensor.rectangular_directSum_rank_of_injective
{K : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
{A : Type u_4}
{B : Type u_5}
{C : Type u_6}
{A' : Type u_7}
{B' : Type u_8}
{C' : Type u_9}
[CommSemiring K]
[DecidableEq ι]
[DecidableEq κ]
[DecidableEq A]
[DecidableEq B]
[DecidableEq C]
[DecidableEq A']
[DecidableEq B']
[DecidableEq C']
{R : ℕ}
(h : (Foundation.Tensor.directSum fun (x : ι) => Foundation.Tensor.matrixCoefficients A B C).RankAtMost R)
(e : κ → ι)
(he : Function.Injective e)
(f : A' → A)
(hf : Function.Injective f)
(g : B' → B)
(hg : Function.Injective g)
(j : C' → C)
(hj : Function.Injective j)
:
(Foundation.Tensor.directSum fun (x : κ) => Foundation.Tensor.matrixCoefficients A' B' C').RankAtMost R
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Tensor.rectangular_directSum_power_rank
{K : Type u_1}
[CommSemiring K]
{a b c L R t : ℕ}
(h :
((Foundation.Tensor.directSum fun (x : Fin L) => Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin c)).power
t).RankAtMost
R)
:
(Foundation.Tensor.directSum fun (x : Fin (L ^ t)) =>
Foundation.Tensor.matrixCoefficients (Fin (a ^ t)) (Fin (b ^ t)) (Fin (c ^ t))).RankAtMost
R
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Tensor.rectangular_pow_batchRank
{K : Type u_1}
[CommSemiring K]
{a b c L r : ℕ}
(hL : 0 < L)
(hbatch :
(Foundation.Tensor.directSum fun (x : Fin L) =>
Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin c)).RankAtMost
r)
(t : ℕ)
:
(Foundation.Tensor.matrixCoefficients (Fin (a ^ t)) (Fin (b ^ t)) (Fin (c ^ t))).RankAtMost (Foundation.batchRank L r t)
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Tensor.rectangular_polynomial_power_rank
{K : Type u_1}
[Field K]
[CharZero K]
{a b c L r d D : ℕ}
(P :
(Foundation.Tensor.directSum fun (x : Fin L) =>
Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin c)).PolynomialApproximation
r d D)
(t : ℕ)
:
(Foundation.Tensor.directSum fun (x : Fin (L ^ t)) =>
Foundation.Tensor.matrixCoefficients (Fin (a ^ t)) (Fin (b ^ t)) (Fin (c ^ t))).RankAtMost
((D * t + 1) * r ^ t)
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Tensor.rectangular_directSum_cyclic_rank
{K : Type u_1}
{ι : Type u_2}
{A : Type u_3}
{B : Type u_4}
{C : Type u_5}
[CommSemiring K]
[DecidableEq ι]
[DecidableEq A]
[DecidableEq B]
[DecidableEq C]
{r : ℕ}
(h : (Foundation.Tensor.directSum fun (x : ι) => Foundation.Tensor.matrixCoefficients A B C).RankAtMost r)
:
(Foundation.Tensor.directSum fun (x : ι) => Foundation.Tensor.matrixCoefficients B C A).RankAtMost r
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.Tensor.rectangular_directSum_rank_lower
{K : Type u_1}
[Field K]
{a b L r : ℕ}
(ha : 0 < a)
(hb : 0 < b)
(h :
(Foundation.Tensor.directSum fun (x : Fin L) =>
Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin a)).RankAtMost
r)
: