Rectangular matrix multiplication algorithms and their asymptotic exponents.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rectangularTagEquiv (L : ℕ) : Fin (L ^ 3) ≃ (Fin L × Fin L) × Fin L

Identify a standard set of L cubed tags with three independent L-valued tags.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rectangularTagEquiv L = Fintype.equivOfCardEq ⋯

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rectangularIndexEquiv (a b c : ℕ) : Fin (a * b * c) ≃ Fin a × Fin b × Fin c

Identify a standard product-sized index set with the three rectangular coordinate sets.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rectangularIndexEquiv a b c = Fintype.equivOfCardEq ⋯

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_directSum_symmetrized_rank {a b c L r : ℕ} (h : (directSum fun (x : Fin L) => matrixMultiplication a b c).RankAtMost r) : (directSum fun (x : Fin (L ^ 3)) => matrixMultiplication (a * b * c) (a * b * c) (a * b * c)).RankAtMost (r ^ 3)

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixCoefficientsDirectSumOfInjective {F : Type u_1} {ι : Type u_2} {κ : Type u_3} {A : Type u_4} {B : Type u_5} [Field F] [DecidableEq ι] [DecidableEq κ] [DecidableEq A] [DecidableEq B] {r d D : ℕ} (P : (directSum fun (x : ι) => matrixCoefficients A A A).PolynomialApproximation r d D) (f : κ → ι) (hf : Function.Injective f) (g : B → A) (hg : Function.Injective g) : (directSum fun (x : κ) => matrixCoefficients B B B).PolynomialApproximation r d D

Pull a direct-sum matrix tensor approximation back along injective tag and coordinate maps.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixMultiplicationDirectSumSymmetrized {a b c L r d D : ℕ} (P : (directSum fun (x : Fin L) => matrixMultiplication a b c).PolynomialApproximation r d D) : (directSum fun (x : Fin (L ^ 3)) => matrixMultiplication (a * b * c) (a * b * c) (a * b * c)).PolynomialApproximation (r ^ 3) (3 * d) (3 * D)

Symmetrize a direct sum of finite rectangular matrix multiplication tensors into square ones.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.mul_rpow_third_le_of_cube {u v w r : ℝ} (hv : 0 ≤ v) (hr : 0 ≤ r) (h : u ^ 3 * v ^ w ≤ r ^ 3) : u * v ^ (w / 3) ≤ r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.equalRectangular_inequality {a b c L r : ℕ} (ha : 1 ≤ a) (hb : 1 ≤ b) (hc : 1 ≤ c) (h : (Tensor.directSum fun (x : Fin L) => Tensor.matrixMultiplication a b c).RankAtMost r) : ↑L * ↑(a * b * c) ^ (omega / 3) ≤ ↑r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.equalRectangular_inequality_of_polynomialApproximation {a b c L r d D : ℕ} (ha : 1 ≤ a) (hb : 1 ≤ b) (hc : 1 ≤ c) (P : (Tensor.directSum fun (x : Fin L) => Tensor.matrixMultiplication a b c).PolynomialApproximation r d D) : ↑L * ↑(a * b * c) ^ (omega / 3) ≤ ↑r