Matrix multiplication exponent

StructureRank-one trilinear term#✓fully proved

For a type \(F\) with multiplication and types \(A\), \(B\), \(C\), a rank-one trilinear term is a triple of functions \(u : A \to F\), \(v : B \to F\), \(w : C \to F\) (its left, middle and right factors), representing one rank-one summand \(u \otimes v \otimes w\) of a trilinear tensor decomposition.

structure RankOneTrilinearTerm (F : Type u) (A : Type v) (B : Type w) (C : Type x)
    [Mul F] where
  left : A → F
  middle : B → F
  right : C → F

Used by 9

Used byValue of a rank-one trilinear term · Tensor rank at most \(r\) · Tensor rank bounds agree with coefficient rank bounds · Trilinear rank at most \(r\) · Trivial upper bound on trilinear rank · Direct rank bound for the matrix multiplication tensor · Monotonicity of trilinear rank bounds · Strassen's rank bound for \(2 \times 2\) matrix multiplication · The pure tensor of a rank-one term

DefinitionValue of a rank-one trilinear term#✓fully proved

For a rank-one trilinear term over a semigroup \(F\) with factors \(u : A \to F\), \(v : B \to F\) and \(w : C \to F\), its value at \(a \in A\), \(b \in B\), \(c \in C\) is the product \(u(a)\,v(b)\,w(c)\).

def RankOneTrilinearTerm.eval {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Semigroup F] (term : RankOneTrilinearTerm F A B C) (a : A) (b : B) (c : C) : F :=
  term.left a * term.middle b * term.right c

Uses 1 · Used by 6

Statement usesRank-one trilinear term

Used byTensor rank bounds agree with coefficient rank bounds · Trilinear rank at most \(r\) · Trivial upper bound on trilinear rank · Direct rank bound for the matrix multiplication tensor · Monotonicity of trilinear rank bounds · Strassen's rank bound for \(2 \times 2\) matrix multiplication

DefinitionTrilinear rank at most \(r\)#✓fully proved

Let \(F\) be a semiring and \(A\), \(B\), \(C\) types. An array \(T : A \to B \to C \to F\) has trilinear rank at most \(r\) when there are \(s \le r\) and functions \(u_i : A \to F\), \(v_i : B \to F\), \(w_i : C \to F\) for \(i = 1, \dots, s\) such that \(T(a, b, c) = \sum_{i=1}^{s} u_i(a)\,v_i(b)\,w_i(c)\) for all \(a \in A\), \(b \in B\), \(c \in C\).

def HasTrilinearRankAtMost {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Semiring F] (T : A → B → C → F) (r : ℕ) : Prop :=
  ∃ terms : List (RankOneTrilinearTerm F A B C), terms.length ≤ r ∧
    ∀ a b c, T a b c = (terms.map fun term ↦ term.eval a b c).sum

Uses 2 · Used by 19

Statement usesRank-one trilinear term · Value of a rank-one trilinear term

Used byMatrix multiplication rank exponent · Rank exponents via the minimum tensor rank · Exponent three for matrix multiplication rank · Rank exponents for rectangular matrix multiplication · Tensor rank bounds agree with coefficient rank bounds · Trivial upper bound on trilinear rank · Rank bounds via the trilinear rank · Direct decomposition of the structure tensor · Strassen's decomposition of the structure tensor · Direct rank bound for the matrix multiplication tensor · Monotonicity of trilinear rank bounds · Monotonicity of matrix multiplication rank exponents · Strassen's rank bound for \(2 \times 2\) matrix multiplication · Direct rank bound for the square matrix multiplication tensor · Decompositions bound the tensor rank · The tensor rank is attained · Trilinear rank · Decompositions bound the trilinear rank · The trilinear rank is attained

TheoremMonotonicity of trilinear rank bounds#✓fully proved

Let \(F\) be a semiring and \(T : A \to B \to C \to F\) an array. If \(T\) has trilinear rank at most \(r\) and \(r \le s\), then \(T\) has trilinear rank at most \(s\).

theorem HasTrilinearRankAtMost.mono {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Semiring F] {T : A → B → C → F} {r s : ℕ}
    (h : HasTrilinearRankAtMost T r) (hrs : r ≤ s) : HasTrilinearRankAtMost T s

Uses 3 · Used by 1

Statement usesTrilinear rank at most \(r\)

Proof usesRank-one trilinear term · Value of a rank-one trilinear term

Used byRank bounds via the trilinear rank

TheoremTrivial upper bound on trilinear rank#✓fully proved

Let \(F\) be a semiring and \(A\), \(B\), \(C\) finite types. Every array \(T : A \to B \to C \to F\) has trilinear rank at most \(|A| \cdot |B| \cdot |C|\).

theorem hasTrilinearRankAtMost_card {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Semiring F] [Fintype A] [Fintype B] [Fintype C] (T : A → B → C → F) :
    HasTrilinearRankAtMost T (Fintype.card A * Fintype.card B * Fintype.card C)

Uses 3 · Used by 3

Statement usesTrilinear rank at most \(r\)

Proof usesRank-one trilinear term · Value of a rank-one trilinear term

Used byTrilinear rank · Decompositions bound the trilinear rank · The trilinear rank is attained

DefinitionTrilinear rank#✓fully proved

Let \(F\) be a semiring and let \(A\), \(B\), \(C\) be finite types. The trilinear rank of a coefficient array \(T : A \to B \to C \to F\) is the least \(r \in \mathbb{N}\) for which there are \(s \le r\) functions \(u_i : A \to F\), \(v_i : B \to F\), \(w_i : C \to F\) with \(T(a, b, c) = \sum_{i=1}^{s} u_i(a)\,v_i(b)\,w_i(c)\) for all \(a \in A\), \(b \in B\), \(c \in C\).

Such an \(r\) exists because \(|A| \cdot |B| \cdot |C|\) coordinate terms always suffice.

noncomputable def trilinearRank {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Semiring F] [Fintype A] [Fintype B] [Fintype C] (T : A → B → C → F) : ℕ := by
  classical
  exact Nat.find ⟨_, hasTrilinearRankAtMost_card T⟩

Uses 2 · Used by 6

Statement usesTrilinear rank at most \(r\) · Trivial upper bound on trilinear rank

Used byRank exponents via the minimum tensor rank · Rank bounds via the trilinear rank · Square matrix multiplication rank equals the coefficient tensor rank · Tensor rank · Decompositions bound the trilinear rank · The trilinear rank is attained

TheoremThe trilinear rank is attained#✓fully proved

Let \(F\) be a semiring, let \(A\), \(B\), \(C\) be finite types, let \(T : A \to B \to C \to F\) be a coefficient array, and let \(R(T)\) be its trilinear rank. Then there are \(s \le R(T)\) functions \(u_i : A \to F\), \(v_i : B \to F\), \(w_i : C \to F\) with \(T(a, b, c) = \sum_{i=1}^{s} u_i(a)\,v_i(b)\,w_i(c)\) for all \(a \in A\), \(b \in B\), \(c \in C\).

theorem trilinearRank_spec {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Semiring F] [Fintype A] [Fintype B] [Fintype C] (T : A → B → C → F) :
    HasTrilinearRankAtMost T (trilinearRank T)

Uses 3 · Used by 3

Statement usesTrilinear rank at most \(r\) · Trilinear rank

Proof usesTrivial upper bound on trilinear rank

Used byRank exponents via the minimum tensor rank · Rank bounds via the trilinear rank · The tensor rank is attained

TheoremDecompositions bound the trilinear rank#✓fully proved

Let \(F\) be a semiring, let \(A\), \(B\), \(C\) be finite types, and let \(T : A \to B \to C \to F\) be a coefficient array. If there are \(s \le r\) functions \(u_i : A \to F\), \(v_i : B \to F\), \(w_i : C \to F\) with \(T(a, b, c) = \sum_{i=1}^{s} u_i(a)\,v_i(b)\,w_i(c)\) for all \(a \in A\), \(b \in B\), \(c \in C\), then the trilinear rank of \(T\) is at most \(r\).

theorem trilinearRank_le {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Semiring F] [Fintype A] [Fintype B] [Fintype C] {T : A → B → C → F} {r : ℕ}
    (h : HasTrilinearRankAtMost T r) : trilinearRank T ≤ r

Uses 3 · Used by 3

Statement usesTrilinear rank at most \(r\) · Trilinear rank

Proof usesTrivial upper bound on trilinear rank

Used byRank exponents via the minimum tensor rank · Rank bounds via the trilinear rank · Decompositions bound the tensor rank

TheoremRank bounds via the trilinear rank#✓fully proved

Let \(F\) be a semiring and \(A\), \(B\), \(C\) finite types. For every array \(T : A \to B \to C \to F\) and every natural number \(r\), \(T\) has trilinear rank at most \(r\) if and only if the trilinear rank of \(T\) (the least length of a decomposition of \(T\) into rank-one arrays) is at most \(r\).

theorem hasTrilinearRankAtMost_iff {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Semiring F] [Fintype A] [Fintype B] [Fintype C] (T : A → B → C → F) (r : ℕ) :
    HasTrilinearRankAtMost T r ↔ trilinearRank T ≤ r

Uses 5

Statement usesTrilinear rank at most \(r\) · Trilinear rank

Proof usesMonotonicity of trilinear rank bounds · Decompositions bound the trilinear rank · The trilinear rank is attained

AbbreviationTrilinear tensors#✓fully proved

For a field \(F\) and types \(A\), \(B\), \(C\), write \(F^X\) for the \(F\)-vector space of functions \(X \to F\). The space of trilinear tensors over \(F\) indexed by \(A\), \(B\), \(C\) is the tensor product \((F^A \otimes_F F^B) \otimes_F F^C\) over \(F\).

abbrev TrilinearTensor (F : Type u) [Field F] (A : Type v) (B : Type w) (C : Type x) :=
  ((A → F) ⊗[F] (B → F)) ⊗[F] (C → F)

Used by 13

Used byTensor rank at most \(r\) · Tensor rank bounds agree with coefficient rank bounds · Matrix multiplication structure tensor · Coefficients of the matrix multiplication structure tensor · Direct decomposition of the structure tensor · Strassen's decomposition of the structure tensor · Square matrix multiplication rank equals the coefficient tensor rank · The pure tensor of a rank-one term · Tensor rank · Decompositions bound the tensor rank · The tensor rank is attained · Coefficient array of a trilinear tensor · Coefficients of a pure tensor

DefinitionCoefficient array of a trilinear tensor#✓fully proved

Let \(F\) be a field, let \(A\) and \(C\) be finite types, let \(B\) be a type, and write \(F^X\) for the space of functions \(X \to F\). The coefficient map is the \(F\)-linear isomorphism from \((F^A \otimes_F F^B) \otimes_F F^C\) to the space of arrays \(A \to B \to C \to F\) that sends each pure tensor \((u \otimes v) \otimes w\) to the array \((a, b, c) \mapsto u(a)\,v(b)\,w(c)\).

Cslib.Complexity.Algebraic.MatrixMultiplicationExponent.trilinearTensorCoefficients · 15 lines

noncomputable def trilinearTensorCoefficients (F : Type u) [Field F]
    (A : Type v) (B : Type w) (C : Type x) [Fintype A] [Fintype C] :
    TrilinearTensor F A B C ≃ₗ[F] (A → B → C → F) := by
  classical
  exact (TensorProduct.piScalarRight F F ((A → F) ⊗[F] (B → F)) C).trans
    ((LinearEquiv.piCongrRight fun _ ↦
      (TensorProduct.comm F (A → F) (B → F)).trans
        (TensorProduct.piScalarRight F F (B → F) A)).trans {
      toFun f a b c := f c a b
      invFun f c a b := f a b c
      left_inv _ := rfl
      right_inv _ := rfl
      map_add' _ _ := rfl
      map_smul' _ _ := rfl
    })

Uses 1 · Used by 9

Statement usesTrilinear tensors

Used byTensor rank bounds agree with coefficient rank bounds · Coefficients of the matrix multiplication structure tensor · Direct decomposition of the structure tensor · Strassen's decomposition of the structure tensor · Square matrix multiplication rank equals the coefficient tensor rank · Tensor rank · Decompositions bound the tensor rank · The tensor rank is attained · Coefficients of a pure tensor

TheoremCoefficients of a pure tensor#✓fully proved

Let \(F\) be a field, let \(A\) and \(C\) be finite types and let \(B\) be a type. For \(u : A \to F\), \(v : B \to F\), \(w : C \to F\) and \(a \in A\), \(b \in B\), \(c \in C\), the coefficient array of the pure tensor \((u \otimes v) \otimes w\) takes the value \(u(a)\,v(b)\,w(c)\) at \((a, b, c)\).

@[simp] theorem trilinearTensorCoefficients_tmul (F : Type u) [Field F]
    (A : Type v) (B : Type w) (C : Type x) [Fintype A] [Fintype C]
    (left : A → F) (middle : B → F) (right : C → F) (a : A) (b : B) (c : C) :
    trilinearTensorCoefficients F A B C ((left ⊗ₜ[F] middle) ⊗ₜ[F] right) a b c =
      left a * middle b * right c

Uses 2 · Used by 2

Statement usesTrilinear tensors · Coefficient array of a trilinear tensor

Used byTensor rank bounds agree with coefficient rank bounds · Coefficients of the matrix multiplication structure tensor

DefinitionThe pure tensor of a rank-one term#✓fully proved

Let \(F\) be a field and \(A\), \(B\), \(C\) types. A rank-one trilinear term with factors \(u : A \to F\), \(v : B \to F\) and \(w : C \to F\) determines the pure tensor \((u \otimes v) \otimes w\) in the trilinear tensor space over \(F\) indexed by \(A\), \(B\), \(C\).

def RankOneTrilinearTerm.tensor {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Field F] (term : RankOneTrilinearTerm F A B C) : TrilinearTensor F A B C :=
  (term.left ⊗ₜ[F] term.middle) ⊗ₜ[F] term.right

Uses 2 · Used by 2

Statement usesRank-one trilinear term · Trilinear tensors

Used byTensor rank at most \(r\) · Tensor rank bounds agree with coefficient rank bounds

DefinitionTensor rank at most \(r\)#✓fully proved

Let \(F\) be a field and \(A\), \(B\), \(C\) types. An element \(T\) of \((F^A \otimes_F F^B) \otimes_F F^C\) has tensor rank at most \(r\) when there are \(s \le r\) and functions \(u_i : A \to F\), \(v_i : B \to F\), \(w_i : C \to F\) for \(i = 1, \dots, s\) such that \(T = \sum_{i=1}^{s} (u_i \otimes v_i) \otimes w_i\).

def HasTensorRankAtMost {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Field F] (T : TrilinearTensor F A B C) (r : ℕ) : Prop :=
  ∃ terms : List (RankOneTrilinearTerm F A B C), terms.length ≤ r ∧
    T = (terms.map RankOneTrilinearTerm.tensor).sum

Uses 3 · Used by 5

Statement usesRank-one trilinear term · The pure tensor of a rank-one term · Trilinear tensors

Used byTensor rank bounds agree with coefficient rank bounds · Direct decomposition of the structure tensor · Strassen's decomposition of the structure tensor · Decompositions bound the tensor rank · The tensor rank is attained

TheoremTensor rank bounds agree with coefficient rank bounds#✓fully proved

Let \(F\) be a field and \(A\), \(B\), \(C\) types with \(A\) and \(C\) finite, and let \(T\) be an element of \((F^A \otimes_F F^B) \otimes_F F^C\). For every natural number \(r\), \(T\) has tensor rank at most \(r\) if and only if its coefficient array \(A \to B \to C \to F\), obtained by the canonical linear equivalence, has trilinear rank at most \(r\).

theorem hasTensorRankAtMost_iff {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Field F] [Fintype A] [Fintype C] (T : TrilinearTensor F A B C) (r : ℕ) :
    HasTensorRankAtMost T r ↔
      HasTrilinearRankAtMost (trilinearTensorCoefficients F A B C T) r

Uses 8 · Used by 4

Statement usesTensor rank at most \(r\) · Trilinear rank at most \(r\) · Trilinear tensors · Coefficient array of a trilinear tensor

Proof usesRank-one trilinear term · Value of a rank-one trilinear term · The pure tensor of a rank-one term · Coefficients of a pure tensor

Used byDirect decomposition of the structure tensor · Strassen's decomposition of the structure tensor · Decompositions bound the tensor rank · The tensor rank is attained

DefinitionTensor rank#✓fully proved

Let \(F\) be a field and let \(A\), \(B\), \(C\) be finite types. The tensor rank of a trilinear tensor \(T\) over \(F\) indexed by \(A\), \(B\), \(C\) is the least \(r \in \mathbb{N}\) such that \(T\) is a sum of at most \(r\) pure tensors \((u \otimes v) \otimes w\) with \(u : A \to F\), \(v : B \to F\) and \(w : C \to F\).

It is defined as the trilinear rank of the coefficient array of \(T\).

noncomputable def tensorRank {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Field F] [Fintype A] [Fintype B] [Fintype C] (T : TrilinearTensor F A B C) : ℕ :=
  trilinearRank (trilinearTensorCoefficients F A B C T)

Uses 3 · Used by 3

Statement usesTrilinear tensors · Trilinear rank · Coefficient array of a trilinear tensor

Used bySquare matrix multiplication rank · Decompositions bound the tensor rank · The tensor rank is attained

TheoremThe tensor rank is attained#✓fully proved

Let \(F\) be a field, let \(A\), \(B\), \(C\) be finite types, let \(T\) be a trilinear tensor over \(F\) indexed by \(A\), \(B\), \(C\), and let \(R(T)\) be its tensor rank. Then \(T\) is a sum of at most \(R(T)\) pure tensors \((u \otimes v) \otimes w\) with \(u : A \to F\), \(v : B \to F\) and \(w : C \to F\).

theorem tensorRank_spec {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Field F] [Fintype A] [Fintype B] [Fintype C] (T : TrilinearTensor F A B C) :
    HasTensorRankAtMost T (tensorRank T)

Uses 7

Statement usesTensor rank at most \(r\) · Trilinear tensors · Tensor rank

Proof usesTrilinear rank at most \(r\) · Tensor rank bounds agree with coefficient rank bounds · The trilinear rank is attained · Coefficient array of a trilinear tensor

TheoremDecompositions bound the tensor rank#✓fully proved

Let \(F\) be a field, let \(A\), \(B\), \(C\) be finite types, and let \(T\) be a trilinear tensor over \(F\) indexed by \(A\), \(B\), \(C\). If \(T\) is a sum of at most \(r\) pure tensors \((u \otimes v) \otimes w\) with \(u : A \to F\), \(v : B \to F\) and \(w : C \to F\), then the tensor rank of \(T\) is at most \(r\).

theorem tensorRank_le {F : Type u} {A : Type v} {B : Type w} {C : Type x}
    [Field F] [Fintype A] [Fintype B] [Fintype C] {T : TrilinearTensor F A B C} {r : ℕ}
    (h : HasTensorRankAtMost T r) : tensorRank T ≤ r

Uses 7

Statement usesTensor rank at most \(r\) · Trilinear tensors · Tensor rank

Proof usesTrilinear rank at most \(r\) · Tensor rank bounds agree with coefficient rank bounds · Decompositions bound the trilinear rank · Coefficient array of a trilinear tensor

AbbreviationMatrix coordinates#✓fully proved

The index set of an \(m \times n\) matrix: pairs \((i, j)\) of a row index \(i \in \{0, \dots, m-1\}\) and a column index \(j \in \{0, \dots, n-1\}\).

abbrev MatrixCoordinate (m n : ℕ) := Fin m × Fin n

Used by 18

Used byMatrix multiplication rank exponent · Rank exponents via the minimum tensor rank · Exponent three for matrix multiplication rank · Rank exponents for rectangular matrix multiplication · Matrix multiplication structure tensor · Coefficients of the matrix multiplication structure tensor · Direct decomposition of the structure tensor · Strassen's decomposition of the structure tensor · Matrix multiplication tensor · Matrix multiplication tensor contraction · Contracting the matrix multiplication tensor gives the matrix product · Direct rank bound for the matrix multiplication tensor · Monotonicity of matrix multiplication rank exponents · Square matrix multiplication rank · Square matrix multiplication rank equals the coefficient tensor rank · Square matrix multiplication tensor · Strassen's rank bound for \(2 \times 2\) matrix multiplication · Direct rank bound for the square matrix multiplication tensor

DefinitionMatrix multiplication tensor#✓fully proved

For a field \(F\) and natural numbers \(m\), \(n\), \(p\), the matrix multiplication tensor is the array over \(F\) indexed by triples \(((i, j), (j', k), (k', i'))\) of an \(m \times n\), an \(n \times p\) and a \(p \times m\) matrix coordinate, whose entry is \(1\) if \(j = j'\), \(k = k'\) and \(i' = i\), and \(0\) otherwise.

These are the coefficients of \(\sum_{i, j, k} e_{(i,j)} \otimes e_{(j,k)} \otimes e_{(k,i)}\), the tensor of multiplying an \(m \times n\) matrix by an \(n \times p\) matrix.

def matrixMultiplicationTensor (F : Type u) [Field F] (m n p : ℕ) :
    MatrixCoordinate m n → MatrixCoordinate n p → MatrixCoordinate p m → F :=
  fun a b c ↦ if a.2 = b.1 ∧ b.2 = c.1 ∧ c.2 = a.1 then 1 else 0

Uses 1 · Used by 9

Statement usesMatrix coordinates

Used byRank exponents for rectangular matrix multiplication · Coefficients of the matrix multiplication structure tensor · Direct decomposition of the structure tensor · Strassen's decomposition of the structure tensor · Matrix multiplication tensor contraction · Contracting the matrix multiplication tensor gives the matrix product · Direct rank bound for the matrix multiplication tensor · Square matrix multiplication rank equals the coefficient tensor rank · Square matrix multiplication tensor

DefinitionSquare matrix multiplication tensor#✓fully proved

For a field \(F\) and a natural number \(n\), the square matrix multiplication tensor over \(F\) is the matrix multiplication tensor for multiplying an \(n \times n\) matrix by an \(n \times n\) matrix. Its value at a triple of matrix coordinates \(((i, j), (j', k), (k', i'))\) is \(1\) when \(j = j'\), \(k = k'\) and \(i = i'\), and \(0\) otherwise.

def squareMatrixMultiplicationTensor (F : Type u) [Field F] (n : ℕ) :
    MatrixCoordinate n n → MatrixCoordinate n n → MatrixCoordinate n n → F :=
  matrixMultiplicationTensor F n n n

Uses 2 · Used by 7

Statement usesMatrix coordinates · Matrix multiplication tensor

Used byMatrix multiplication rank exponent · Rank exponents via the minimum tensor rank · Exponent three for matrix multiplication rank · Monotonicity of matrix multiplication rank exponents · Square matrix multiplication rank equals the coefficient tensor rank · Strassen's rank bound for \(2 \times 2\) matrix multiplication · Direct rank bound for the square matrix multiplication tensor

DefinitionMatrix multiplication structure tensor#✓fully proved

For a field \(F\) and natural numbers \(m, n, p\), the structure tensor of multiplying an \(m \times n\) matrix by an \(n \times p\) matrix over \(F\) is the element \(\sum_{i < m} \sum_{j < n} \sum_{k < p} e_{(i,j)} \otimes e_{(j,k)} \otimes e_{(k,i)}\) of the trilinear tensor space \(F^{[m] \times [n]} \otimes F^{[n] \times [p]} \otimes F^{[p] \times [m]}\), where \([m] = \{0, \dots, m - 1\}\) and \(e_x\) is the standard basis vector at the matrix coordinate \(x\).

noncomputable def matrixMultiplicationStructureTensor (F : Type u) [Field F] (m n p : ℕ) :
    TrilinearTensor F (MatrixCoordinate m n) (MatrixCoordinate n p) (MatrixCoordinate p m) :=
  ∑ i : Fin m, ∑ j : Fin n, ∑ k : Fin p,
    (Pi.single (i, j) (1 : F) ⊗ₜ[F] Pi.single (j, k) (1 : F)) ⊗ₜ[F]
      Pi.single (k, i) (1 : F)

Uses 2 · Used by 5

Statement usesMatrix coordinates · Trilinear tensors

Used byCoefficients of the matrix multiplication structure tensor · Direct decomposition of the structure tensor · Strassen's decomposition of the structure tensor · Square matrix multiplication rank · Square matrix multiplication rank equals the coefficient tensor rank

TheoremCoefficients of the matrix multiplication structure tensor#✓fully proved

Let \(F\) be a field, let \(m, n, p\) be natural numbers, and write \(e_x\) for the standard basis vector with index \(x\). The coordinates of the structure tensor \(\sum_{i < m,\, j < n,\, k < p} e_{(i,j)} \otimes e_{(j,k)} \otimes e_{(k,i)}\) in \(F^{m \times n} \otimes F^{n \times p} \otimes F^{p \times m}\) are the matrix multiplication coefficients: the coordinate at \(((i, j), (j', k), (k', i'))\) is \(1\) if \(j = j'\), \(k = k'\) and \(i = i'\), and \(0\) otherwise.

theorem matrixMultiplicationStructureTensor_coefficients (F : Type u) [Field F] (m n p : ℕ) :
    trilinearTensorCoefficients F _ _ _ (matrixMultiplicationStructureTensor F m n p) =
      matrixMultiplicationTensor F m n p

Uses 6 · Used by 3

Statement usesMatrix coordinates · Trilinear tensors · Matrix multiplication structure tensor · Matrix multiplication tensor · Coefficient array of a trilinear tensor

Proof usesCoefficients of a pure tensor

Used byDirect decomposition of the structure tensor · Strassen's decomposition of the structure tensor · Square matrix multiplication rank equals the coefficient tensor rank

DefinitionSquare matrix multiplication rank#✓fully proved

For a field \(F\) and a natural number \(n\), the square matrix multiplication rank of \(F\) at \(n\) is the tensor rank of the structure tensor of multiplying two \(n \times n\) matrices over \(F\): the least number of pure tensors whose sum is that structure tensor.

noncomputable def squareMatrixMultiplicationRank (F : Type u) [Field F] (n : ℕ) : ℕ :=
  tensorRank (matrixMultiplicationStructureTensor F n n n)

Uses 3 · Used by 2

Statement usesMatrix coordinates · Matrix multiplication structure tensor · Tensor rank

Used byRank exponents via the minimum tensor rank · Square matrix multiplication rank equals the coefficient tensor rank

TheoremSquare matrix multiplication rank equals the coefficient tensor rank#✓fully proved

For every field \(F\) and natural number \(n\), the square matrix multiplication rank of \(F\) at \(n\) equals the trilinear rank of the square \(n \times n\) matrix multiplication tensor over \(F\).

theorem squareMatrixMultiplicationRank_eq (F : Type u) [Field F] (n : ℕ) :
    squareMatrixMultiplicationRank F n = trilinearRank (squareMatrixMultiplicationTensor F n)

Uses 9 · Used by 1

Statement usesMatrix coordinates · Square matrix multiplication rank · Square matrix multiplication tensor · Trilinear rank

Proof usesTrilinear tensors · Matrix multiplication structure tensor · Coefficients of the matrix multiplication structure tensor · Matrix multiplication tensor · Coefficient array of a trilinear tensor

Used byRank exponents via the minimum tensor rank

DefinitionMatrix multiplication tensor contraction#✓fully proved

Let \(F\) be a field, let \(m, n, p\) be natural numbers, let \(A \in F^{m \times n}\) and \(B \in F^{n \times p}\), and let \(i < m\) and \(k < p\). Write \(T\) for the matrix multiplication tensor over \(F\) for \(m, n, p\) and, for a natural number \(q\), \([q] = \{0, \dots, q - 1\}\). The contraction of \(T\) against \(A\) and \(B\) at output coordinate \((i, k)\) is

\[\sum_{a \in [m] \times [n]} \sum_{b \in [n] \times [p]} T(a, b, (k, i)) \, A_a \, B_b,\]

where \(A_a\) and \(B_b\) are the entries of \(A\) and \(B\) at the matrix coordinates \(a\) and \(b\).

noncomputable def matrixMultiplicationTensorContraction (F : Type u) [Field F]
    {m n p : ℕ} (A : Matrix (Fin m) (Fin n) F) (B : Matrix (Fin n) (Fin p) F)
    (i : Fin m) (k : Fin p) : F :=
  ∑ a : MatrixCoordinate m n, ∑ b : MatrixCoordinate n p,
    matrixMultiplicationTensor F m n p a b (k, i) * A a.1 a.2 * B b.1 b.2

Uses 2 · Used by 1

Statement usesMatrix coordinates · Matrix multiplication tensor

Used byContracting the matrix multiplication tensor gives the matrix product

TheoremContracting the matrix multiplication tensor gives the matrix product#✓fully proved

For a field \(F\), matrices \(A \in F^{m \times n}\) and \(B \in F^{n \times p}\), and indices \(i < m\) and \(k < p\), the contraction of the matrix multiplication tensor against \(A\) and \(B\) at output coordinate \((i, k)\) equals the entry \((AB)_{ik}\) of the matrix product.

theorem matrixMultiplicationTensorContraction_eq_mul (F : Type u) [Field F]
    {m n p : ℕ} (A : Matrix (Fin m) (Fin n) F) (B : Matrix (Fin n) (Fin p) F)
    (i : Fin m) (k : Fin p) :
    matrixMultiplicationTensorContraction F A B i k = (A * B) i k

Uses 3

Statement usesMatrix multiplication tensor contraction

Proof usesMatrix coordinates · Matrix multiplication tensor

DefinitionMatrix multiplication rank exponent#✓fully proved

A real number \(w\) is a matrix multiplication rank exponent over a field \(F\) when \(w \ge 0\) and there are a real \(C > 0\) and a natural number \(N_0 \ge 1\) such that for every \(n \ge N_0\) the \(n \times n\) matrix multiplication coefficient tensor over \(F\) is a sum of at most \(C n^w\) rank-one trilinear terms.

def HasMatrixMultiplicationRankExponent (F : Type u) [Field F] (w : ℝ) : Prop :=
  0 ≤ w ∧ ∃ C : ℝ, 0 < C ∧ ∃ N₀ : ℕ, 1 ≤ N₀ ∧
    ∀ n : ℕ, N₀ ≤ n → ∃ r : ℕ,
      HasTrilinearRankAtMost (squareMatrixMultiplicationTensor F n) r ∧
        (r : ℝ) ≤ C * Real.rpow (n : ℝ) w

Uses 3 · Used by 10

Statement usesTrilinear rank at most \(r\) · Matrix coordinates · Square matrix multiplication tensor

Used byRank exponents via the minimum tensor rank · Exponent three for matrix multiplication rank · Exponents above the matrix multiplication exponent admit rank bounds · Lower bounds for the matrix multiplication exponent · Matrix multiplication exponent · Rank bounds just above the matrix multiplication exponent · Upper bounds on the matrix multiplication exponent · Rank exponents bound the matrix multiplication exponent · The matrix multiplication exponent is at most three · Monotonicity of matrix multiplication rank exponents

TheoremRank exponents via the minimum tensor rank#✓fully proved

Let \(F\) be a field and \(w\) a real number. Then \(w\) is a matrix multiplication rank exponent over \(F\) if and only if \(w \ge 0\) and there are a real \(C > 0\) and a natural number \(N_0 \ge 1\) such that for every \(n \ge N_0\) the tensor rank of the \(n \times n\) matrix multiplication structure tensor over \(F\) is at most \(C n^w\).

theorem hasMatrixMultiplicationRankExponent_iff (F : Type u) [Field F] (w : ℝ) :
    HasMatrixMultiplicationRankExponent F w ↔
      0 ≤ w ∧ ∃ C : ℝ, 0 < C ∧ ∃ N₀ : ℕ, 1 ≤ N₀ ∧
        ∀ n : ℕ, N₀ ≤ n →
          (squareMatrixMultiplicationRank F n : ℝ) ≤ C * Real.rpow (n : ℝ) w

Uses 9

Statement usesMatrix multiplication rank exponent · Square matrix multiplication rank

Proof usesTrilinear rank at most \(r\) · Matrix coordinates · Square matrix multiplication rank equals the coefficient tensor rank · Square matrix multiplication tensor · Trilinear rank · Decompositions bound the trilinear rank · The trilinear rank is attained

TheoremMonotonicity of matrix multiplication rank exponents#✓fully proved

Let \(F\) be a field and let \(w \le w'\) be real numbers. If \(w\) is a matrix multiplication rank exponent for \(F\), then so is \(w'\).

theorem HasMatrixMultiplicationRankExponent.mono (F : Type u) [Field F] {w w' : ℝ}
    (h : HasMatrixMultiplicationRankExponent F w) (hww' : w ≤ w') :
    HasMatrixMultiplicationRankExponent F w'

Uses 4 · Used by 1

Statement usesMatrix multiplication rank exponent

Proof usesTrilinear rank at most \(r\) · Matrix coordinates · Square matrix multiplication tensor

Used byExponents above the matrix multiplication exponent admit rank bounds

DefinitionMatrix multiplication exponent#✓fully proved

The matrix multiplication exponent \(\omega(F)\) of a field \(F\) is the infimum, taken in \([0, \infty]\), of the real numbers \(w\) that are matrix multiplication rank exponents over \(F\); it is \(\infty\) when there is no such \(w\).

noncomputable def matrixMultiplicationExponent (F : Type u) [Field F] : ENNReal :=
  sInf {W : ENNReal | ∃ w : ℝ, W = ENNReal.ofReal w ∧
    HasMatrixMultiplicationRankExponent F w}

Uses 1 · Used by 8

Statement usesMatrix multiplication rank exponent

Used byExponents above the matrix multiplication exponent admit rank bounds · Lower bounds for the matrix multiplication exponent · Rank bounds just above the matrix multiplication exponent · Upper bounds on the matrix multiplication exponent · Rank exponents bound the matrix multiplication exponent · The matrix multiplication exponent is at most three · The matrix multiplication exponent is finite · Circuit size and tensor rank give the same square exponent

TheoremRank exponents bound the matrix multiplication exponent#✓fully proved

If a real number \(w\) is a matrix multiplication rank exponent over a field \(F\), then the matrix multiplication exponent \(\omega(F)\) of \(F\) satisfies \(\omega(F) \le w\).

theorem matrixMultiplicationExponent_le_of_admissible (F : Type u) [Field F] {w : ℝ}
    (h : HasMatrixMultiplicationRankExponent F w) :
    matrixMultiplicationExponent F ≤ ENNReal.ofReal w

Uses 2 · Used by 1

Statement usesMatrix multiplication rank exponent · Matrix multiplication exponent

Used byUpper bounds on the matrix multiplication exponent

TheoremLower bounds for the matrix multiplication exponent#✓fully proved

Let \(F\) be a field and let \(W\) be an element of \([0, \infty]\). If \(W \le w\) for every real number \(w\) that is a matrix multiplication rank exponent over \(F\), then \(W\) is at most the matrix multiplication exponent \(\omega(F)\).

theorem le_matrixMultiplicationExponent (F : Type u) [Field F] {W : ENNReal}
    (h : ∀ w : ℝ, HasMatrixMultiplicationRankExponent F w → W ≤ ENNReal.ofReal w) :
    W ≤ matrixMultiplicationExponent F

Uses 2

Statement usesMatrix multiplication rank exponent · Matrix multiplication exponent

TheoremDirect rank bound for the matrix multiplication tensor#✓fully proved

For every field \(F\) and natural numbers \(m, n, p\), the coefficient tensor of multiplying an \(m \times n\) matrix by an \(n \times p\) matrix over \(F\) is a sum of at most \(mnp\) rank-one trilinear terms.

The decomposition is the direct algorithm, with one term for each triple \((i, j, k)\) with \(i < m\), \(j < n\) and \(k < p\).

theorem matrixMultiplicationTensor_rank_le_product (F : Type u) [Field F] (m n p : ℕ) :
    HasTrilinearRankAtMost (matrixMultiplicationTensor F m n p) (m * n * p)

Uses 5 · Used by 2

Statement usesTrilinear rank at most \(r\) · Matrix coordinates · Matrix multiplication tensor

Proof usesRank-one trilinear term · Value of a rank-one trilinear term

Used byDirect decomposition of the structure tensor · Direct rank bound for the square matrix multiplication tensor

TheoremDirect decomposition of the structure tensor#✓fully proved

Let \(F\) be a field, let \(m, n, p\) be natural numbers, and write \(e_x\) for the standard basis vector with index \(x\). The matrix multiplication structure tensor \(\sum_{i < m,\, j < n,\, k < p} e_{(i,j)} \otimes e_{(j,k)} \otimes e_{(k,i)}\) in \(F^{m \times n} \otimes F^{n \times p} \otimes F^{p \times m}\) is a sum of at most \(mnp\) pure tensors \(u \otimes v \otimes w\).

theorem matrixMultiplicationStructureTensor_rank_le_product (F : Type u) [Field F] (m n p : ℕ) :
    HasTensorRankAtMost (matrixMultiplicationStructureTensor F m n p) (m * n * p)

Uses 10

Statement usesTensor rank at most \(r\) · Matrix coordinates · Matrix multiplication structure tensor

Proof usesTrilinear rank at most \(r\) · Trilinear tensors · Tensor rank bounds agree with coefficient rank bounds · Coefficients of the matrix multiplication structure tensor · Matrix multiplication tensor · Direct rank bound for the matrix multiplication tensor · Coefficient array of a trilinear tensor

TheoremStrassen's rank bound for \(2 \times 2\) matrix multiplication#✓fully proved

For every field \(F\), the square \(2 \times 2\) matrix multiplication tensor over \(F\) is a sum of at most \(7\) rank-one trilinear terms.

The seven terms are Strassen's, and the decomposition holds in every characteristic.

theorem squareMatrixMultiplicationTensor_rank_le_seven (F : Type u) [Field F] :
    HasTrilinearRankAtMost (squareMatrixMultiplicationTensor F 2) 7

Uses 5 · Used by 1

Statement usesTrilinear rank at most \(r\) · Matrix coordinates · Square matrix multiplication tensor

Proof usesRank-one trilinear term · Value of a rank-one trilinear term

Used byStrassen's decomposition of the structure tensor

TheoremStrassen's decomposition of the structure tensor#✓fully proved

Let \(F\) be a field and write \(e_x\) for the standard basis vector with index \(x\). The \(2 \times 2\) matrix multiplication structure tensor \(\sum_{i, j, k < 2} e_{(i,j)} \otimes e_{(j,k)} \otimes e_{(k,i)}\) in \(F^{2 \times 2} \otimes F^{2 \times 2} \otimes F^{2 \times 2}\) is a sum of at most \(7\) pure tensors \(u \otimes v \otimes w\).

theorem matrixMultiplicationStructureTensor_rank_le_seven (F : Type u) [Field F] :
    HasTensorRankAtMost (matrixMultiplicationStructureTensor F 2 2 2) 7

Uses 10

Statement usesTensor rank at most \(r\) · Matrix coordinates · Matrix multiplication structure tensor

Proof usesTrilinear rank at most \(r\) · Trilinear tensors · Tensor rank bounds agree with coefficient rank bounds · Coefficients of the matrix multiplication structure tensor · Matrix multiplication tensor · Strassen's rank bound for \(2 \times 2\) matrix multiplication · Coefficient array of a trilinear tensor

TheoremDirect rank bound for the square matrix multiplication tensor#✓fully proved

For every field \(F\) and natural number \(n\), the square \(n \times n\) matrix multiplication tensor over \(F\) is a sum of at most \(n^3\) rank-one trilinear terms.

theorem squareMatrixMultiplicationTensor_rank_le_cube (F : Type u) [Field F] (n : ℕ) :
    HasTrilinearRankAtMost (squareMatrixMultiplicationTensor F n) (n * n * n)

Uses 4 · Used by 1

Statement usesTrilinear rank at most \(r\) · Matrix coordinates · Square matrix multiplication tensor

Proof usesDirect rank bound for the matrix multiplication tensor

Used byExponent three for matrix multiplication rank

TheoremExponent three for matrix multiplication rank#✓fully proved

For every field \(F\), the number \(3\) is a matrix multiplication rank exponent over \(F\).

It is witnessed by the direct decomposition of the \(n \times n\) matrix multiplication tensor into \(n^3\) rank-one terms.

theorem hasMatrixMultiplicationRankExponent_three (F : Type u) [Field F] :
    HasMatrixMultiplicationRankExponent F 3

Uses 5 · Used by 1

Statement usesMatrix multiplication rank exponent

Proof usesTrilinear rank at most \(r\) · Matrix coordinates · Square matrix multiplication tensor · Direct rank bound for the square matrix multiplication tensor

Used byThe matrix multiplication exponent is at most three

TheoremThe matrix multiplication exponent is at most three#✓fully proved

For every field \(F\), the matrix multiplication exponent \(\omega(F)\) of \(F\) satisfies \(\omega(F) \le 3\).

theorem matrixMultiplicationExponent_le_three (F : Type u) [Field F] :
    matrixMultiplicationExponent F ≤ ENNReal.ofReal 3

Uses 3 · Used by 1

Statement usesMatrix multiplication exponent

Proof usesMatrix multiplication rank exponent · Exponent three for matrix multiplication rank

Used byThe matrix multiplication exponent is finite

TheoremThe matrix multiplication exponent is finite#✓fully proved

For every field \(F\), the matrix multiplication exponent of \(F\), an element of \([0, \infty]\), is not \(\infty\).

theorem matrixMultiplicationExponent_ne_top (F : Type u) [Field F] :
    matrixMultiplicationExponent F ≠ ⊤

Uses 2 · Used by 2

Statement usesMatrix multiplication exponent

Proof usesThe matrix multiplication exponent is at most three

Used byRank bounds just above the matrix multiplication exponent · Upper bounds on the matrix multiplication exponent

TheoremExponents above the matrix multiplication exponent admit rank bounds#✓fully proved

Let \(F\) be a field, let \(\omega(F)\) be its matrix multiplication exponent and let \(w > 0\) be real. If \(\omega(F) < w\), then there are \(C > 0\) and \(N_0 \ge 1\) such that for every \(n \ge N_0\) the \(n \times n\) matrix multiplication tensor over \(F\) has rank at most \(C n^w\).

theorem hasMatrixMultiplicationRankExponent_of_inf_lt (F : Type u) [Field F] {w : ℝ}
    (hw : 0 < w) (h : matrixMultiplicationExponent F < ENNReal.ofReal w) :
    HasMatrixMultiplicationRankExponent F w

Uses 3 · Used by 1

Statement usesMatrix multiplication rank exponent · Matrix multiplication exponent

Proof usesMonotonicity of matrix multiplication rank exponents

Used byUpper bounds on the matrix multiplication exponent

TheoremUpper bounds on the matrix multiplication exponent#✓fully proved

Let \(F\) be a field, let \(\omega(F)\) be its matrix multiplication exponent and let \(w \ge 0\) be real. Then \(\omega(F) \le w\) if and only if for every real \(\varepsilon > 0\) there are \(C > 0\) and \(N_0 \ge 1\) such that for every \(n \ge N_0\) the \(n \times n\) matrix multiplication tensor over \(F\) has rank at most \(C n^{w + \varepsilon}\).

The right-hand side bounds the rank by \(C n^{w + \varepsilon}\) for each \(\varepsilon > 0\); it is not an \(O(n^w)\) rank bound.

theorem matrixMultiplicationExponent_le_iff (F : Type u) [Field F] (w : ℝ) (hw : 0 ≤ w) :
    matrixMultiplicationExponent F ≤ ENNReal.ofReal w ↔
      ∀ ε : ℝ, 0 < ε → HasMatrixMultiplicationRankExponent F (w + ε)

Uses 5 · Used by 1

Statement usesMatrix multiplication rank exponent · Matrix multiplication exponent

Proof usesExponents above the matrix multiplication exponent admit rank bounds · Rank exponents bound the matrix multiplication exponent · The matrix multiplication exponent is finite

Used byRank bounds just above the matrix multiplication exponent

TheoremRank bounds just above the matrix multiplication exponent#✓fully proved

Let \(F\) be a field and let \(\omega(F)\) be its matrix multiplication exponent, a finite real number. For every real \(\varepsilon > 0\) there are \(C > 0\) and \(N_0 \ge 1\) such that for every \(n \ge N_0\) the \(n \times n\) matrix multiplication tensor over \(F\) has rank at most \(C n^{\omega(F) + \varepsilon}\).

theorem matrixMultiplicationExponent_endpoint (F : Type u) [Field F] :
    ∀ ε : ℝ, 0 < ε →
      HasMatrixMultiplicationRankExponent F ((matrixMultiplicationExponent F).toReal + ε)

Uses 4

Statement usesMatrix multiplication rank exponent · Matrix multiplication exponent

Proof usesUpper bounds on the matrix multiplication exponent · The matrix multiplication exponent is finite

DefinitionRectangular inner dimension#✓fully proved

For a natural number \(n\) and a real aspect \(k\), the rectangular inner dimension is \(\lceil n^k \rceil\), the least natural number that is at least the real power \(n^k\).

It is the inner dimension in the product of an \(n \times \lceil n^k \rceil\) matrix and a \(\lceil n^k \rceil \times n\) matrix.

noncomputable def rectangularInnerDimension (n : ℕ) (k : ℝ) : ℕ :=
  Nat.ceil (Real.rpow (n : ℝ) k)

Used by 10

Used byAdmissible rectangular circuit exponents · Exponent two is admissible at aspect zero · Admissible circuit exponents are upward closed · Upper bounds on the rectangular circuit exponent · The rounded inner dimension is positive · Admissible rectangular circuit exponents are at least two · Rank exponents for rectangular matrix multiplication · Rectangular inner dimension at aspect one · Rectangular inner dimension at dimension one · Rectangular inner dimension at aspect zero

TheoremRectangular inner dimension at aspect zero#✓fully proved

For every natural number \(n\), including \(n = 0\), the rectangular inner dimension at dimension \(n\) and aspect \(0\), namely \(\lceil n^0 \rceil\), equals \(1\), so aspect \(0\) is the outer product of an \(n \times 1\) matrix and a \(1 \times n\) matrix.

@[simp] theorem rectangularInnerDimension_zero (n : ℕ) :
    rectangularInnerDimension n 0 = 1

Uses 1 · Used by 1

Statement usesRectangular inner dimension

Used byExponent two is admissible at aspect zero

TheoremRectangular inner dimension at aspect one#✓fully proved

For every natural number \(n\), the rectangular inner dimension at dimension \(n\) and aspect \(1\), namely \(\lceil n^1 \rceil\), equals \(n\), so aspect \(1\) is square matrix multiplication without rounding.

@[simp] theorem rectangularInnerDimension_one (n : ℕ) :
    rectangularInnerDimension n 1 = n

Uses 1

Statement usesRectangular inner dimension

TheoremRectangular inner dimension at dimension one#✓fully proved

For every real aspect \(k\), the rectangular inner dimension at dimension \(1\) and aspect \(k\), namely \(\lceil 1^k \rceil\), equals \(1\).

@[simp] theorem rectangularInnerDimension_one_base (k : ℝ) :
    rectangularInnerDimension 1 k = 1

Uses 1

Statement usesRectangular inner dimension

DefinitionRank exponents for rectangular matrix multiplication#✓fully proved

Let \(F\) be a field and let \(k, w\) be real. Then \(w\) is a rank exponent for rectangular matrix multiplication over \(F\) at aspect \(k\) when \(k \ge 0\), \(w \ge 0\), and for every \(\varepsilon > 0\) there are \(C > 0\) and \(N_0 \ge 1\) such that for every \(n \ge N_0\) the tensor of multiplying an \(n \times \lceil n^k \rceil\) matrix by a \(\lceil n^k \rceil \times n\) matrix over \(F\) has rank at most \(C n^{w + \varepsilon}\).

The coefficient \(C\) and the threshold \(N_0\) may depend on \(\varepsilon\), but not on \(n\).

def HasRectangularMatrixMultiplicationRankExponent (F : Type u) [Field F]
    (k w : ℝ) : Prop :=
  0 ≤ k ∧ 0 ≤ w ∧ ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧ ∃ N₀ : ℕ, 1 ≤ N₀ ∧
    ∀ n : ℕ, N₀ ≤ n → ∃ r : ℕ,
      HasTrilinearRankAtMost
        (matrixMultiplicationTensor F n (rectangularInnerDimension n k) n) r ∧
      (r : ℝ) ≤ C * Real.rpow (n : ℝ) (w + ε)

Uses 4 · Used by 1

Statement usesTrilinear rank at most \(r\) · Matrix coordinates · Matrix multiplication tensor · Rectangular inner dimension

Used byRectangular matrix multiplication exponent

DefinitionRectangular matrix multiplication exponent#✓fully proved

For a field \(F\) and a real number \(k\), the rectangular matrix multiplication exponent \(\omega(k)\) of \(F\) is the infimum in \([0, \infty]\) of all real \(w \ge 0\) with the following property: for every \(\varepsilon > 0\) there are a real \(C > 0\) and a natural number \(N_0 \ge 1\) such that for every \(n \ge N_0\), the coefficient tensor \(\sum e_{ij} \otimes e_{jl} \otimes e_{li}\) of multiplying an \(n \times \lceil n^k \rceil\) matrix by an \(\lceil n^k \rceil \times n\) matrix over \(F\) is a sum of at most \(C n^{w + \varepsilon}\) rank-one trilinear terms. If \(k < 0\), no \(w\) qualifies and \(\omega(k) = \infty\).

noncomputable def rectangularMatrixMultiplicationExponent (F : Type u) [Field F]
    (k : ℝ) : ENNReal :=
  sInf {W : ENNReal | ∃ w : ℝ, W = ENNReal.ofReal w ∧
    HasRectangularMatrixMultiplicationRankExponent F k w}

Uses 1 · Used by 2

Statement usesRank exponents for rectangular matrix multiplication

Used byDual matrix multiplication exponent · Circuit size and tensor rank give the same rectangular exponent

DefinitionDual matrix multiplication exponent#✓fully proved

For a field \(F\), the dual matrix multiplication exponent of \(F\) is the supremum, taken in the extended nonnegative reals \([0, \infty]\), of the set of real aspects \(k \ge 0\) for which the rectangular matrix multiplication exponent of \(F\) at aspect \(k\) equals \(2\).

noncomputable def dualMatrixMultiplicationExponent (F : Type u) [Field F] : ENNReal :=
  sSup {K : ENNReal | ∃ k : ℝ, 0 ≤ k ∧ K = ENNReal.ofReal k ∧
    rectangularMatrixMultiplicationExponent F k = 2}

Uses 1

Statement usesRectangular matrix multiplication exponent

TheoremDual exponent at most one#●ready to prove

For every field \(F\), the dual matrix multiplication exponent \(\alpha(F)\) of the arithmetic-circuit model satisfies \(\alpha(F) \le 1\).

theorem_wanted upperBoundOne :
    ∀ (F : Type u) [Field F], dualCircuitExponent F ≤ 1

Sources

• C15b, CLLZ2025 Figure 2, the general upper bound, not a method-specific barrier.

Uses 1

Statement usesDual matrix multiplication exponent (arithmetic circuits)

TheoremCoppersmith's rectangular exponent#●ready to prove

For every field \(F\), the rectangular matrix multiplication exponent of the arithmetic-circuit model at aspect \(0.172\) equals \(2\): an \(n \times \lceil n^{0.172} \rceil\) matrix times an \(\lceil n^{0.172} \rceil \times n\) matrix costs \(n^{2 + o(1)}\) arithmetic operations.

theorem_wanted coppersmith1982Exponent :
    ∀ (F : Type u) [Field F], rectangularCircuitExponent F ((172 : ℝ) / 1000) = 2

Sources

• C15b/LGU2018 Section 1.1, Coppersmith's 1982 exponent equality.

Uses 1

Statement usesRectangular circuit exponent

TheoremCoppersmith's 1997 bound on the dual exponent#●ready to prove

For every field \(F\), the dual matrix multiplication exponent \(\alpha(F)\) of the arithmetic-circuit model satisfies \(\alpha(F) > 0.29462\).

theorem_wanted coppersmith1997StrictLower :
    ∀ (F : Type u) [Field F], ENNReal.ofReal ((29462 : ℝ) / 100000) < dualCircuitExponent F

Sources

• C15b/LG2012 abstract, the previous Coppersmith 1997 record is strict.

Uses 1

Statement usesDual matrix multiplication exponent (arithmetic circuits)

TheoremLe Gall's 2012 bound on the dual exponent#●ready to prove

For every field \(F\), the dual matrix multiplication exponent \(\alpha(F)\) of the arithmetic-circuit model satisfies \(\alpha(F) > 0.30298\).

theorem_wanted leGall2012StrictLower :
    ∀ (F : Type u) [Field F], ENNReal.ofReal ((30298 : ℝ) / 100000) < dualCircuitExponent F

Sources

• C15b/LG2012 abstract, Le Gall's 2012 improvement is strict.

Uses 1

Statement usesDual matrix multiplication exponent (arithmetic circuits)

TheoremLe Gall–Urrutia bound on the dual exponent#●ready to prove

For every field \(F\), the dual matrix multiplication exponent \(\alpha(F)\) of the arithmetic-circuit model satisfies \(\alpha(F) \ge 0.31389\).

theorem_wanted leGallUrrutia2018Lower :
    ∀ (F : Type u) [Field F], ENNReal.ofReal ((31389 : ℝ) / 100000) ≤ dualCircuitExponent F

Sources

• C15b/LGU2018 Section 1.2, the fourth-power lower bound is weak.

Uses 1

Statement usesDual matrix multiplication exponent (arithmetic circuits)

TheoremWilliams–Xu–Xu–Zhou bound on the dual exponent#●ready to prove

For every field \(F\), the dual matrix multiplication exponent \(\alpha(F)\) of the arithmetic-circuit model satisfies \(\alpha(F) > 0.321334\).

theorem_wanted williamsXuXuZhou2024StrictLower :
    ∀ (F : Type u) [Field F], ENNReal.ofReal ((321334 : ℝ) / 1000000) < dualCircuitExponent F

Sources

• C15b/WXXZ2024 introduction, the best displayed lower bound is strict.

Uses 1

Statement usesDual matrix multiplication exponent (arithmetic circuits)

TheoremNaive bound for rectangular matrix multiplication#●ready to prove

For every field \(F\) and every real \(k \ge 0\), the rectangular matrix multiplication exponent of the arithmetic-circuit model at aspect \(k\) is at most \(2 + k\).

theorem_wanted rectangularNaiveUpper :
    ∀ (F : Type u) [Field F] (k : ℝ), 0 ≤ k →
      rectangularCircuitExponent F k ≤ ENNReal.ofReal (2 + k)

Sources

• CLLZ rectangular naive upper bound; a general finite circuit construction is missing.

Uses 1

Statement usesRectangular circuit exponent

TheoremCircuit size and tensor rank give the same rectangular exponent#●ready to prove

For every field \(F\) and every real \(k \ge 0\), the rectangular matrix multiplication exponent at aspect \(k\) defined by arithmetic-circuit size equals the one defined by tensor rank.

theorem_wanted rectangularOperationRankBridge :
    ∀ (F : Type u) [Field F] (k : ℝ), 0 ≤ k →
      rectangularCircuitExponent F k =
        MatrixMultiplicationExponent.rectangularMatrixMultiplicationExponent F k

Sources

• LG2012 exact bilinear-rank characterization; the operation/rank transfer is missing.

Uses 2

Statement usesRectangular matrix multiplication exponent · Rectangular circuit exponent

TheoremThe rectangular exponent depends only on the characteristic#●ready to prove

If two fields \(F\) and \(K\) have the same characteristic, then for every real \(k \ge 0\) the rectangular matrix multiplication exponents of \(F\) and \(K\) in the arithmetic-circuit model at aspect \(k\) are equal.

theorem_wanted characteristicInvariance :
    ∀ (F : Type u) (K : Type v) [Field F] [Field K], ringChar F = ringChar K →
      ∀ k : ℝ, 0 ≤ k → rectangularCircuitExponent F k = rectangularCircuitExponent K k

Sources

• LG2012 Section 1, characteristic dependence; this circuit-model transfer is missing.

Uses 1

Statement usesRectangular circuit exponent

DefinitionConjecture that the square exponent is two#✓fully proved

The proposition that for every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model equals \(2\).

Since \(\omega(F) \ge 2\) always holds, this says the trivial lower bound is sharp. It is a conjecture, recorded as a proposition and not asserted.

def omegaEqualsTwoConjecture : Prop :=
  ∀ (F : Type u) [Field F], squareMatrixMultiplicationCircuitExponent F = 2

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremNaive bound for square matrix multiplication#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 3\).

theorem_wanted naiveUpperThree :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤ ENNReal.ofReal 3

Sources

• C15a, trivial upper bound. The general finite naive circuit construction is not supplied upstream, so this remains a proof request.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremStrassen's 1969 bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le \log_2 7\).

theorem_wanted strassen1969Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal (Real.log 7 / Real.log 2)

Sources

• C15a [S1969], Strassen's log₂ 7 bound.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremPan's 1978 bound on the square exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le \log_{70} 143640\).

theorem_wanted pan1978Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal (Real.log 143640 / Real.log 70)

Sources

• C15a [P1978], Pan's log₇₀ 143640 bound.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremBini–Capovani–Romani–Lotti bound on the square exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 3 \log_{12} 10\).

theorem_wanted biniCapovaniRomaniLotti1979Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal (3 * (Real.log 10 / Real.log 12))

Sources

• C15a [BCRL1979, B1980], the 3 log₁₂ 10 approximate-algorithm bound.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremPan's 1979 bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 3 \log_{436} 196\).

theorem_wanted pan1979Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal (3 * (Real.log 196 / Real.log 436))

Sources

• C15a [P1979], Pan's 3 log₄₃₆ 196 bound.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremPan's 1980 bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le \log_{48} 47216\).

theorem_wanted pan1980Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal (Real.log 47216 / Real.log 48)

Sources

• C15a [P1980], Pan's log₄₈ 47216 bound.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremSchönhage's 1981 bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le \log_{110} 140600\).

theorem_wanted schonhage1981Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal (Real.log 140600 / Real.log 110)

Sources

• C15a [S1981], Schönhage's log₁₁₀ 140600 bound.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremPan's 1981 bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.5161\).

theorem_wanted pan1981Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((25161 : ℝ) / 10000)

Sources

• C15a [P1981], Pan's decimal bound 2.5161.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremRomani's 1982 bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.5166\).

theorem_wanted romani1982Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((25166 : ℝ) / 10000)

Sources

• C15a [R1982], Romani's decimal bound 2.5166.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremCoppersmith–Winograd 1982 bound on the square exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.495548\).

theorem_wanted coppersmithWinograd1982Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((2495548 : ℝ) / 1000000)

Sources

• C15a [CW1982], Coppersmith--Winograd bound 2.495548.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremStrassen's 1987 bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.4785\).

theorem_wanted strassen1987Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((24785 : ℝ) / 10000)

Sources

• C15a [S1987], Strassen's laser-method bound 2.4785.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremCoppersmith–Winograd 1990 bound on the square exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.375477\).

theorem_wanted coppersmithWinograd1990Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((2375477 : ℝ) / 1000000)

Sources

• C15a [CW1990], Coppersmith--Winograd bound 2.375477.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremCohn–Kleinberg–Szegedy–Umans bound on the square exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.41\).

theorem_wanted cohnKleinbergSzegedyUmans2005Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((241 : ℝ) / 100)

Sources

• C15a [CKSU2005], group-theoretic bound 2.41.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremStothers–Davie bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.373689703\).

theorem_wanted stothersDavie2013Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((2373689703 : ℝ) / 1000000000)

Sources

• C15a [S2010, DS2013], bound 2.373689703.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremVassilevska Williams's 2012 bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.372873\).

theorem_wanted vassilevskaWilliams2012Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((2372873 : ℝ) / 1000000)

Sources

• C15a [V2012, V2014], Vassilevska Williams bound 2.372873.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremZhdanovich's 2012 bound on the matrix multiplication exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.373\).

theorem_wanted zhdanovich2012Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((2373 : ℝ) / 1000)

Sources

• C15a [Z2012], Zhdanovich bound 2.373.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremLe Gall's 2014 bound on the square exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.3728639\).

theorem_wanted leGall2014Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((23728639 : ℝ) / 10000000)

Sources

• C15a [LG2014], Le Gall bound 2.3728639.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremAlman–Vassilevska Williams 2020 bound on the square exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.3728596\).

theorem_wanted almanVassilevskaWilliams2020Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((23728596 : ℝ) / 10000000)

Sources

• C15a [AV2020], Alman--Vassilevska Williams bound 2.3728596.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremDuan–Wu–Zhou bound on the square exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent \(\omega(F)\) of the arithmetic-circuit model satisfies \(\omega(F) \le 2.371866\).

theorem_wanted duanWuZhou2022Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((2371866 : ℝ) / 1000000)

Sources

• C15a [DWZ2022], Duan--Wu--Zhou bound 2.371866.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremVassilevska Williams–Xu–Xu–Zhou upper bound for matrix multiplication#●ready to prove

For every field \(F\), the square matrix multiplication exponent of \(F\) in the arithmetic-circuit model is at most \(2.371552\).

theorem_wanted vassilevskaWilliamsXuXuZhou2023Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((2371552 : ℝ) / 1000000)

Sources

• C15a [VXXZ2023], bound 2.371552.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremAlman–Duan–Vassilevska Williams–Xu–Xu–Zhou upper bound for matrix multiplication#●ready to prove

For every field \(F\), the square matrix multiplication exponent of \(F\) in the arithmetic-circuit model is at most \(2.371339\).

theorem_wanted almanDuanVassilevskaWilliamsXuXuZhou2024Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((2371339 : ℝ) / 1000000)

Sources

• C15a [ADVXXZ2024], bound 2.371339.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremDupont–Eisenberger et al. upper bound for matrix multiplication#●ready to prove

For every field \(F\), the square matrix multiplication exponent of \(F\) in the arithmetic-circuit model is at most \(2.371177\).

theorem_wanted dupontEisenbergerEtAl2026Upper :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F ≤
        ENNReal.ofReal ((2371177 : ℝ) / 1000000)

Sources

• C15a [DEKMRSZAWB2026], best catalogue bound 2.371177.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

TheoremCircuit size and tensor rank give the same square exponent#●ready to prove

For every field \(F\), the square matrix multiplication exponent of \(F\) defined by arithmetic-circuit size equals the matrix multiplication exponent of \(F\) defined by tensor rank.

theorem_wanted squareOperationRankBridge :
    ∀ (F : Type u) [Field F],
      squareMatrixMultiplicationCircuitExponent F =
        MatrixMultiplicationExponent.matrixMultiplicationExponent F

Sources

• C15a additional comments and [B2013]: the arithmetic-operation exponent agrees with the tensor-rank exponent. This bridge is not proved.

Uses 2

Statement usesMatrix multiplication exponent · Square matrix multiplication circuit exponent

TheoremThe square exponent depends only on the characteristic#●ready to prove

If two fields \(F\) and \(K\) have the same characteristic, then the square matrix multiplication exponents of \(F\) and \(K\) in the arithmetic-circuit model are equal.

theorem_wanted characteristicInvariance :
    ∀ (F : Type u) (K : Type v) [Field F] [Field K], ringChar F = ringChar K →
      squareMatrixMultiplicationCircuitExponent F =
        squareMatrixMultiplicationCircuitExponent K

Sources

• C15a additional comments and [S1981]: the exponent depends only on the field characteristic. This circuit-model transfer is not proved.

Uses 1

Statement usesSquare matrix multiplication circuit exponent

52 fully proved33 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.