Arithmetic circuits for matrix multiplication

AbbreviationMatrix arithmetic circuit#✓fully proved

For a type \(F\) of scalars and \(m, r, n \in \mathbb{N}\), a matrix arithmetic circuit is an arithmetic circuit over \(F\) whose inputs are indexed by the entries \((i, k)\) of an \(m \times r\) matrix together with the entries \((k, j)\) of an \(r \times n\) matrix, and whose outputs are indexed by the entries \((i, j)\) of an \(m \times n\) matrix.

abbrev MatrixArithmeticCircuit (F : Type u) (m r n : ℕ) :=
  ArithmeticCircuit F ((Fin m × Fin r) ⊕ (Fin r × Fin n)) (Fin m × Fin n)

Uses 1 · Used by 9

Statement usesArithmetic circuit

Used byAdmissible rectangular circuit exponents · Exponent two is admissible at aspect zero · Circuits that compute the matrix product · Admissible circuit exponents are upward closed · Outer-product matrix circuit · Lower bound for matrix multiplication circuits · Outputs of a matrix multiplication circuit are gates · Upper bounds on the rectangular circuit exponent · Admissible rectangular circuit exponents are at least two

DefinitionMatrix input assignment#✓fully proved

For matrices \(A \in F^{m \times r}\) and \(B \in F^{r \times n}\), the input assignment of \((A, B)\) is the function on the entry positions \((i, k)\) of an \(m \times r\) matrix together with the entry positions \((k, j)\) of an \(r \times n\) matrix that sends \((i, k)\) to \(A_{ik}\) and \((k, j)\) to \(B_{kj}\). It supplies the inputs of a matrix arithmetic circuit.

def matrixInput {F : Type u} {m r n : ℕ}
    (A : Matrix (Fin m) (Fin r) F) (B : Matrix (Fin r) (Fin n) F) :
    ((Fin m × Fin r) ⊕ (Fin r × Fin n)) → F :=
  Sum.elim (fun p => A p.1 p.2) (fun p => B p.1 p.2)

Used by 4

Used byCircuits that compute the matrix product · The outer-product matrix circuit computes the matrix product · Lower bound for matrix multiplication circuits · Outputs of a matrix multiplication circuit are gates

DefinitionCircuits that compute the matrix product#✓fully proved

A circuit \(c\) over a field \(F\) whose inputs are the entries of an \(m \times r\) matrix and an \(r \times n\) matrix computes matrix multiplication when, for all matrices \(A \in F^{m \times r}\) and \(B \in F^{r \times n}\) and all \(i < m\), \(j < n\), its output at \((i, j)\) on the entries of \(A\) and \(B\) equals \((AB)_{ij}\).

Correctness is required on actual values in \(F\), not as an identity of formal polynomials.

def IsMatrixMultiplication {F : Type u} [Field F] {m r n : ℕ}
    (c : MatrixArithmeticCircuit F m r n) : Prop :=
  ∀ (A : Matrix (Fin m) (Fin r) F) (B : Matrix (Fin r) (Fin n) F)
    (i : Fin m) (j : Fin n), c.evaluate (matrixInput A B) (i, j) = (A * B) i j

Uses 3 · Used by 8

Statement usesCircuit evaluation · Matrix arithmetic circuit · Matrix input assignment

Used byAdmissible rectangular circuit exponents · Exponent two is admissible at aspect zero · Admissible circuit exponents are upward closed · The outer-product matrix circuit computes the matrix product · Lower bound for matrix multiplication circuits · Outputs of a matrix multiplication circuit are gates · Upper bounds on the rectangular circuit exponent · Admissible rectangular circuit exponents are at least two

DefinitionOuter-product matrix circuit#✓fully proved

For a type \(F\) of scalars and \(m, n \in \mathbb{N}\), the outer-product matrix circuit is the matrix arithmetic circuit for an \(m \times 1\) matrix times a \(1 \times n\) matrix with exactly \(mn\) gates: for \(i < m\) and \(j < n\), the gate for \((i, j)\) multiplies the input at entry \((i, 0)\) of the first matrix by the input at entry \((0, j)\) of the second, and the output at \((i, j)\) is that gate.

def outerMatrixCircuit (F : Type u) (m n : ℕ) : MatrixArithmeticCircuit F m 1 n where
  size := (ArithmeticCircuit.outerProduct F m n).size
  gate i := .mul (.input (.inl ((finProdFinEquiv.symm i).1, 0)))
    (.input (.inr (0, (finProdFinEquiv.symm i).2)))
  output ij := .node (finProdFinEquiv ij)

Uses 5 · Used by 3

Statement usesArithmetic circuit · Outer-product circuit · Arithmetic gate · Arithmetic operand · Matrix arithmetic circuit

Used byExponent two is admissible at aspect zero · The outer-product matrix circuit computes the matrix product · Size of the outer-product matrix circuit

TheoremThe outer-product matrix circuit computes the matrix product#✓fully proved

For every field \(F\) and all \(m, n \in \mathbb{N}\), the outer-product matrix circuit over \(F\) computes the product of an \(m \times 1\) matrix and a \(1 \times n\) matrix.

theorem outerMatrixCircuit_correct {F : Type u} [Field F] (m n : ℕ) :
    IsMatrixMultiplication (outerMatrixCircuit F m n)

Uses 10 · Used by 1

Statement usesCircuits that compute the matrix product · Outer-product matrix circuit

Proof usesArithmetic circuit · Circuit evaluation · Value of a gate in a circuit · Arithmetic gate · Gate evaluation · Arithmetic operand · Operand evaluation · Matrix input assignment

Used byExponent two is admissible at aspect zero

TheoremSize of the outer-product matrix circuit#✓fully proved

For every type \(F\) of scalars and all \(m, n \in \mathbb{N}\), the outer-product matrix circuit over \(F\) has exactly \(mn\) gates.

theorem outerMatrixCircuit_size (F : Type u) (m n : ℕ) :
    (outerMatrixCircuit F m n).size = m * n

Uses 2

Statement usesArithmetic circuit · Outer-product matrix circuit

TheoremOutputs of a matrix multiplication circuit are gates#✓fully proved

Let \(F\) be a field and let \(c\) be a circuit over \(F\) that computes the product of an \(m \times r\) matrix and an \(r \times n\) matrix, where \(r \ge 1\). Then for all \(i < m\) and \(j < n\), the output of \(c\) at \((i, j)\) is one of its gates, not a constant or an input.

theorem IsMatrixMultiplication.output_is_node {F : Type u} [Field F] {m r n : ℕ}
    {c : MatrixArithmeticCircuit F m r n} (hc : IsMatrixMultiplication c)
    (k : Fin r) (i : Fin m) (j : Fin n) :
    ∃ t : Fin c.size, c.output (i, j) = .node t

Uses 7 · Used by 1

Statement usesArithmetic circuit · Arithmetic operand · Circuits that compute the matrix product · Matrix arithmetic circuit

Proof usesCircuit evaluation · Value of a gate in a circuit · Matrix input assignment

Used byLower bound for matrix multiplication circuits

TheoremLower bound for matrix multiplication circuits#✓fully proved

Let \(F\) be a field and let \(c\) be a circuit over \(F\) that computes the product of an \(m \times r\) matrix and an \(r \times n\) matrix, where \(r \ge 1\). Then \(c\) has at least \(mn\) gates.

Distinct entries of the product require distinct gates, over every field.

theorem IsMatrixMultiplication.output_cost_le {F : Type u} [Field F] {m r n : ℕ}
    {c : MatrixArithmeticCircuit F m r n} (hc : IsMatrixMultiplication c)
    (k : Fin r) : m * n ≤ c.size

Uses 9 · Used by 1

Statement usesArithmetic circuit · Circuits that compute the matrix product · Matrix arithmetic circuit

Proof usesCircuit evaluation · Value of a gate in a circuit · Arithmetic operand · Operand evaluation · Outputs of a matrix multiplication circuit are gates · Matrix input assignment

Used byAdmissible rectangular circuit exponents are at least two

DefinitionAdmissible rectangular circuit exponents#✓fully proved

Let \(F\) be a field and \(k, w\) real numbers. The exponent \(w\) is admissible at aspect \(k\) over \(F\) when \(k \ge 0\), \(w \ge 0\), and for every \(\varepsilon > 0\) there are a real \(C > 0\) and a natural number \(N \ge 1\) such that for every \(n \ge N\) some arithmetic circuit over \(F\) computes the product of an \(n \times \lceil n^k \rceil\) matrix and an \(\lceil n^k \rceil \times n\) matrix with at most \(C n^{w + \varepsilon}\) gates.

The circuit may depend on \(n\) and \(\varepsilon\), and it must be correct on every pair of matrices with entries in \(F\).

def HasRectangularCircuitExponent (F : Type u) [Field F] (k w : ℝ) : Prop :=
  0 ≤ k ∧ 0 ≤ w ∧ ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 1 ≤ N ∧
    ∀ n : ℕ, N ≤ n → ∃ c : MatrixArithmeticCircuit F n (rectangularInnerDimension n k) n,
      IsMatrixMultiplication c ∧ (c.size : ℝ) ≤ C * (n : ℝ) ^ (w + ε)

Uses 4 · Used by 12

Statement usesArithmetic circuit · Circuits that compute the matrix product · Matrix arithmetic circuit · Rectangular inner dimension

Used byExponents above the circuit exponent are admissible · Exponent two is admissible at aspect zero · Lower bounds for the rectangular circuit exponent · Admissible circuit exponents are upward closed · Rectangular circuit exponent · A finite rectangular circuit exponent is attained · Upper bounds on the rectangular circuit exponent · Admissible exponents bound the rectangular circuit exponent · Upper bounds on the square matrix multiplication circuit exponent · The square matrix multiplication circuit exponent is attained · Admissible rectangular circuit exponents are at least two · The rectangular circuit exponent is at least two

DefinitionRectangular circuit exponent#✓fully proved

For a field \(F\) and a real \(k\), the rectangular circuit exponent of \(F\) at aspect \(k\) is the infimum in \([0, \infty]\) of the admissible rectangular circuit exponents for \(F\) at aspect \(k\): the reals \(w \ge 0\) such that \(k \ge 0\) and, for every \(\varepsilon > 0\), there are \(C > 0\) and \(N \ge 1\) such that for every \(n \ge N\) some arithmetic circuit over \(F\) of size at most \(C n^{w + \varepsilon}\) computes the product of an \(n \times \lceil n^k \rceil\) matrix and a \(\lceil n^k \rceil \times n\) matrix. The infimum of the empty family is \(\infty\); in particular the exponent is \(\infty\) when \(k < 0\).

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

Uses 1 · Used by 17

Statement usesAdmissible rectangular circuit exponents

Used byDual matrix multiplication exponent (arithmetic circuits) · Some aspect has rectangular circuit exponent two · Upper bounds for the dual circuit exponent · Exponents above the circuit exponent are admissible · Aspects with circuit exponent two bound the dual exponent · Lower bounds for the rectangular circuit exponent · A finite rectangular circuit exponent is attained · Upper bounds on the rectangular circuit exponent · Admissible exponents bound the rectangular circuit exponent · The rectangular circuit exponent at aspect zero is two · Square matrix multiplication circuit exponent · The square circuit exponent is the aspect-one rectangular exponent · The rectangular circuit exponent is at least two · The rectangular exponent depends only on the characteristic · Coppersmith's rectangular exponent · Naive bound for rectangular matrix multiplication · Circuit size and tensor rank give the same rectangular exponent

DefinitionDual matrix multiplication exponent (arithmetic circuits)#✓fully proved

For a field \(F\), the dual matrix multiplication exponent \(\alpha(F) \in [0, \infty]\) of the arithmetic-circuit model is the supremum of all real \(k \ge 0\) at which the rectangular matrix multiplication exponent of the arithmetic-circuit model over \(F\) equals \(2\).

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

Uses 1 · Used by 7

Statement usesRectangular circuit exponent

Used byUpper bounds for the dual circuit exponent · Aspects with circuit exponent two bound the dual exponent · Coppersmith's 1997 bound on the dual exponent · Le Gall–Urrutia bound on the dual exponent · Le Gall's 2012 bound on the dual exponent · Dual exponent at most one · Williams–Xu–Xu–Zhou bound on the dual exponent

TheoremAdmissible exponents bound the rectangular circuit exponent#✓fully proved

Let \(F\) be a field and let \(k\) and \(w\) be reals. If \(w\) is an admissible rectangular circuit exponent for \(F\) at aspect \(k\), then the rectangular circuit exponent of \(F\) at aspect \(k\) is at most \(w\).

theorem rectangularCircuitExponent_le_of_admissible (F : Type u) [Field F] {k w : ℝ}
    (h : HasRectangularCircuitExponent F k w) :
    rectangularCircuitExponent F k ≤ ENNReal.ofReal w

Uses 2 · Used by 2

Statement usesAdmissible rectangular circuit exponents · Rectangular circuit exponent

Used byUpper bounds on the rectangular circuit exponent · The rectangular circuit exponent at aspect zero is two

TheoremLower bounds for the rectangular circuit exponent#✓fully proved

Let \(F\) be a field, \(k\) a real number and \(W \in [0, \infty]\). If \(W \le w\) for every real \(w\) that is an admissible exponent at aspect \(k\) over \(F\), then \(W\) is at most the rectangular matrix multiplication exponent of the arithmetic-circuit model over \(F\) at aspect \(k\).

theorem le_rectangularCircuitExponent (F : Type u) [Field F] {k : ℝ} {W : ENNReal}
    (h : ∀ w : ℝ, HasRectangularCircuitExponent F k w → W ≤ ENNReal.ofReal w) :
    W ≤ rectangularCircuitExponent F k

Uses 2 · Used by 1

Statement usesAdmissible rectangular circuit exponents · Rectangular circuit exponent

Used byThe rectangular circuit exponent is at least two

TheoremAspects with circuit exponent two bound the dual exponent#✓fully proved

Let \(F\) be a field and \(k \ge 0\) a real number. If the rectangular matrix multiplication exponent of the arithmetic-circuit model over \(F\) at aspect \(k\) equals \(2\), then \(k \le \alpha(F)\), where \(\alpha(F)\) is the dual matrix multiplication exponent of the arithmetic-circuit model.

theorem le_dualCircuitExponent (F : Type u) [Field F] {k : ℝ} (hk : 0 ≤ k)
    (h : rectangularCircuitExponent F k = 2) : ENNReal.ofReal k ≤ dualCircuitExponent F

Uses 2

Statement usesDual matrix multiplication exponent (arithmetic circuits) · Rectangular circuit exponent

TheoremUpper bounds for the dual circuit exponent#✓fully proved

Let \(F\) be a field and \(K \in [0, \infty]\). If \(k \le K\) for every real \(k \ge 0\) at which the rectangular matrix multiplication exponent of the arithmetic-circuit model over \(F\) equals \(2\), then the dual matrix multiplication exponent \(\alpha(F)\) of the arithmetic-circuit model satisfies \(\alpha(F) \le K\).

theorem dualCircuitExponent_le (F : Type u) [Field F] {K : ENNReal}
    (h : ∀ k : ℝ, 0 ≤ k → rectangularCircuitExponent F k = 2 → ENNReal.ofReal k ≤ K) :
    dualCircuitExponent F ≤ K

Uses 2

Statement usesDual matrix multiplication exponent (arithmetic circuits) · Rectangular circuit exponent

TheoremExponent two is admissible at aspect zero#✓fully proved

For every field \(F\), the exponent \(2\) is an admissible rectangular circuit exponent at aspect \(0\) over \(F\): for every \(\varepsilon > 0\) there are a real \(C > 0\) and a natural number \(N \ge 1\) such that for every \(n \ge N\) some arithmetic circuit over \(F\) computes the product of an \(n \times \lceil n^0 \rceil\) matrix and a \(\lceil n^0 \rceil \times n\) matrix, that is of an \(n \times 1\) matrix and a \(1 \times n\) matrix, with at most \(C n^{2 + \varepsilon}\) gates.

The outer-product circuit, with \(n^2\) gates, is such a circuit.

theorem hasRectangularCircuitExponent_zero_two (F : Type u) [Field F] :
    HasRectangularCircuitExponent F 0 2

Uses 8 · Used by 1

Statement usesAdmissible rectangular circuit exponents

Proof usesArithmetic circuit · Circuits that compute the matrix product · Matrix arithmetic circuit · Rectangular inner dimension · Rectangular inner dimension at aspect zero · Outer-product matrix circuit · The outer-product matrix circuit computes the matrix product

Used byThe rectangular circuit exponent at aspect zero is two

TheoremThe rounded inner dimension is positive#✓fully proved

For every natural number \(n \ge 1\) and every real \(k\), the rounded inner dimension \(\lceil n^k \rceil\) is positive.

theorem rectangularInnerDimension_pos {n : ℕ} (hn : 1 ≤ n) (k : ℝ) :
    0 < rectangularInnerDimension n k

Uses 1 · Used by 1

Statement usesRectangular inner dimension

Used byAdmissible rectangular circuit exponents are at least two

TheoremAdmissible rectangular circuit exponents are at least two#✓fully proved

Let \(F\) be a field and let \(k\) and \(w\) be reals. If \(w\) is an admissible rectangular circuit exponent for \(F\) at aspect \(k\), then \(w \ge 2\).

A circuit computing the product of an \(n \times \lceil n^k \rceil\) matrix and a \(\lceil n^k \rceil \times n\) matrix with \(n \ge 1\) has a separate gate for each of the \(n^2\) output entries, so it has at least \(n^2\) gates.

theorem HasRectangularCircuitExponent.two_le {F : Type u} [Field F] {k w : ℝ}
    (h : HasRectangularCircuitExponent F k w) : 2 ≤ w

Uses 7 · Used by 1

Statement usesAdmissible rectangular circuit exponents

Proof usesArithmetic circuit · Circuits that compute the matrix product · Lower bound for matrix multiplication circuits · Matrix arithmetic circuit · Rectangular inner dimension · The rounded inner dimension is positive

Used byThe rectangular circuit exponent is at least two

TheoremThe rectangular circuit exponent is at least two#✓fully proved

For every field \(F\) and every real \(k\), the rectangular circuit exponent of \(F\) at aspect \(k\) is at least \(2\) (it may be \(\infty\)).

theorem two_le_rectangularCircuitExponent (F : Type u) [Field F] (k : ℝ) :
    2 ≤ rectangularCircuitExponent F k

Uses 4 · Used by 2

Statement usesRectangular circuit exponent

Proof usesAdmissible rectangular circuit exponents · Admissible rectangular circuit exponents are at least two · Lower bounds for the rectangular circuit exponent

Used byThe rectangular circuit exponent at aspect zero is two · The square circuit exponent is at least two

TheoremThe rectangular circuit exponent at aspect zero is two#✓fully proved

For every field \(F\), the rectangular circuit exponent of \(F\) at aspect \(0\) equals \(2\).

The upper bound comes from the outer-product circuit, which multiplies an \(n \times 1\) matrix by a \(1 \times n\) matrix with \(n^2\) multiplications.

theorem rectangularCircuitExponent_zero (F : Type u) [Field F] :
    rectangularCircuitExponent F 0 = 2

Uses 4 · Used by 1

Statement usesRectangular circuit exponent

Proof usesExponent two is admissible at aspect zero · Admissible exponents bound the rectangular circuit exponent · The rectangular circuit exponent is at least two

Used bySome aspect has rectangular circuit exponent two

TheoremSome aspect has rectangular circuit exponent two#✓fully proved

For every field \(F\), there is a real \(k \ge 0\) at which the rectangular matrix multiplication exponent of the arithmetic-circuit model over \(F\) equals \(2\). Hence the set of such \(k\), viewed in \([0, \infty]\), whose supremum is the dual matrix multiplication exponent, is nonempty.

theorem dualCircuitExponent_family_nonempty (F : Type u) [Field F] :
    {K : ENNReal | ∃ k : ℝ, 0 ≤ k ∧ K = ENNReal.ofReal k ∧
      rectangularCircuitExponent F k = 2}.Nonempty

Uses 2

Statement usesRectangular circuit exponent

Proof usesThe rectangular circuit exponent at aspect zero is two

TheoremAdmissible circuit exponents are upward closed#✓fully proved

Let \(F\) be a field and \(k, w, w'\) real numbers with \(w \le w'\). If \(w\) is an admissible exponent at aspect \(k\) over \(F\), then so is \(w'\).

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

Uses 5 · Used by 1

Statement usesAdmissible rectangular circuit exponents

Proof usesArithmetic circuit · Circuits that compute the matrix product · Matrix arithmetic circuit · Rectangular inner dimension

Used byExponents above the circuit exponent are admissible

TheoremExponents above the circuit exponent are admissible#✓fully proved

Let \(F\) be a field and \(k, w\) real numbers with \(w > 0\). If the rectangular matrix multiplication exponent of the arithmetic-circuit model over \(F\) at aspect \(k\) is less than \(w\), then \(w\) is an admissible exponent at aspect \(k\) over \(F\).

theorem hasRectangularCircuitExponent_of_inf_lt (F : Type u) [Field F] {k w : ℝ}
    (hw : 0 < w) (h : rectangularCircuitExponent F k < ENNReal.ofReal w) :
    HasRectangularCircuitExponent F k w

Uses 3 · Used by 1

Statement usesAdmissible rectangular circuit exponents · Rectangular circuit exponent

Proof usesAdmissible circuit exponents are upward closed

Used byUpper bounds on the rectangular circuit exponent

TheoremUpper bounds on the rectangular circuit exponent#✓fully proved

Let \(F\) be a field and let \(k \ge 0\) and \(w \ge 0\) be reals. The rectangular circuit exponent of \(F\) at aspect \(k\) is at most \(w\) if and only if \(w\) is an admissible rectangular circuit exponent for \(F\) at aspect \(k\): for every \(\varepsilon > 0\) there are \(C > 0\) and \(N \ge 1\) such that for every \(n \ge N\) some arithmetic circuit over \(F\) of size at most \(C n^{w + \varepsilon}\) computes the product of an \(n \times \lceil n^k \rceil\) matrix and a \(\lceil n^k \rceil \times n\) matrix.

theorem rectangularCircuitExponent_le_iff (F : Type u) [Field F] {k w : ℝ}
    (hk : 0 ≤ k) (hw : 0 ≤ w) :
    rectangularCircuitExponent F k ≤ ENNReal.ofReal w ↔ HasRectangularCircuitExponent F k w

Uses 8 · Used by 2

Statement usesAdmissible rectangular circuit exponents · Rectangular circuit exponent

Proof usesArithmetic circuit · Circuits that compute the matrix product · Matrix arithmetic circuit · Rectangular inner dimension · Exponents above the circuit exponent are admissible · Admissible exponents bound the rectangular circuit exponent

Used byA finite rectangular circuit exponent is attained · Upper bounds on the square matrix multiplication circuit exponent

TheoremA finite rectangular circuit exponent is attained#✓fully proved

Let \(F\) be a field and \(k \ge 0\) a real number. If the rectangular matrix multiplication exponent \(\omega\) of the arithmetic-circuit model over \(F\) at aspect \(k\) is finite, then \(\omega\) is itself an admissible exponent at aspect \(k\) over \(F\).

theorem rectangularCircuitExponent_endpoint (F : Type u) [Field F] {k : ℝ}
    (hk : 0 ≤ k) (hfinite : rectangularCircuitExponent F k ≠ ⊤) :
    HasRectangularCircuitExponent F k (rectangularCircuitExponent F k).toReal

Uses 3 · Used by 1

Statement usesAdmissible rectangular circuit exponents · Rectangular circuit exponent

Proof usesUpper bounds on the rectangular circuit exponent

Used byThe square matrix multiplication circuit exponent is attained

DefinitionSquare matrix multiplication circuit exponent#✓fully proved

For a field \(F\), the square matrix multiplication circuit exponent of \(F\) is the rectangular circuit exponent of \(F\) at aspect \(1\). Since \(\lceil n^1 \rceil = n\), it is the infimum in \([0, \infty]\) of the reals \(w \ge 0\) such that for every \(\varepsilon > 0\) there are \(C > 0\) and \(N \ge 1\) such that for every \(n \ge N\) some arithmetic circuit over \(F\) of size at most \(C n^{w + \varepsilon}\) computes the product of two \(n \times n\) matrices, and it is \(\infty\) when there is no such \(w\).

noncomputable def squareMatrixMultiplicationCircuitExponent (F : Type u) [Field F] :
    ENNReal :=
  rectangularCircuitExponent F 1

Uses 1 · Used by 29

Statement usesRectangular circuit exponent

Used byThe square circuit exponent is the aspect-one rectangular exponent · Upper bounds on the square matrix multiplication circuit exponent · The square matrix multiplication circuit exponent is attained · The square circuit exponent is at least two · Alman–Duan–Vassilevska Williams–Xu–Xu–Zhou upper bound for matrix multiplication · Alman–Vassilevska Williams 2020 bound on the square exponent · Bini–Capovani–Romani–Lotti bound on the square exponent · The square exponent depends only on the characteristic · Cohn–Kleinberg–Szegedy–Umans bound on the square exponent · Coppersmith–Winograd 1982 bound on the square exponent · Coppersmith–Winograd 1990 bound on the square exponent · Duan–Wu–Zhou bound on the square exponent · Dupont–Eisenberger et al. upper bound for matrix multiplication · Le Gall's 2014 bound on the square exponent · Naive bound for square matrix multiplication · Conjecture that the square exponent is two · Pan's 1978 bound on the square exponent · Pan's 1979 bound on the matrix multiplication exponent · Pan's 1980 bound on the matrix multiplication exponent · Pan's 1981 bound on the matrix multiplication exponent · Romani's 1982 bound on the matrix multiplication exponent · Schönhage's 1981 bound on the matrix multiplication exponent · Circuit size and tensor rank give the same square exponent · Stothers–Davie bound on the matrix multiplication exponent · Strassen's 1969 bound on the matrix multiplication exponent · Strassen's 1987 bound on the matrix multiplication exponent · Vassilevska Williams–Xu–Xu–Zhou upper bound for matrix multiplication · Vassilevska Williams's 2012 bound on the matrix multiplication exponent · Zhdanovich's 2012 bound on the matrix multiplication exponent

TheoremThe square circuit exponent is the aspect-one rectangular exponent#✓fully proved

For every field \(F\), the square matrix multiplication circuit exponent of \(F\) equals the rectangular circuit exponent of \(F\) at aspect \(1\).

theorem squareMatrixMultiplicationCircuitExponent_def (F : Type u) [Field F] :
    squareMatrixMultiplicationCircuitExponent F = rectangularCircuitExponent F 1

Uses 2

Statement usesRectangular circuit exponent · Square matrix multiplication circuit exponent

TheoremThe square circuit exponent is at least two#✓fully proved

For every field \(F\), the square matrix multiplication circuit exponent of \(F\) is at least \(2\).

This trivial bound holds because a circuit computing the product of two \(n \times n\) matrices has a separate gate for each of the \(n^2\) output entries.

theorem two_le_squareMatrixMultiplicationCircuitExponent (F : Type u) [Field F] :
    2 ≤ squareMatrixMultiplicationCircuitExponent F

Uses 2

Statement usesSquare matrix multiplication circuit exponent

Proof usesThe rectangular circuit exponent is at least two

TheoremUpper bounds on the square matrix multiplication circuit exponent#✓fully proved

Let \(F\) be a field with square matrix multiplication circuit exponent \(\omega(F) \in [0, \infty]\), and let \(w \ge 0\) be real. Then \(\omega(F) \le w\) if and only if \(F\) has rectangular circuit exponent \(w\) at aspect \(1\): for every \(\varepsilon > 0\) there are a real \(C > 0\) and a natural number \(N \ge 1\) such that for every \(n \ge N\) some arithmetic circuit over \(F\) with at most \(C n^{w + \varepsilon}\) gates computes the product of every pair of \(n \times n\) matrices over \(F\).

theorem squareMatrixMultiplicationCircuitExponent_le_iff (F : Type u) [Field F]
    {w : ℝ} (hw : 0 ≤ w) :
    squareMatrixMultiplicationCircuitExponent F ≤ ENNReal.ofReal w ↔
      HasRectangularCircuitExponent F 1 w

Uses 3

Statement usesAdmissible rectangular circuit exponents · Square matrix multiplication circuit exponent

Proof usesUpper bounds on the rectangular circuit exponent

TheoremThe square matrix multiplication circuit exponent is attained#✓fully proved

Let \(F\) be a field whose square matrix multiplication circuit exponent \(\omega(F)\) is finite. Then \(F\) has rectangular circuit exponent \(\omega(F)\) at aspect \(1\): for every \(\varepsilon > 0\) there are a real \(C > 0\) and a natural number \(N \ge 1\) such that for every \(n \ge N\) some arithmetic circuit over \(F\) with at most \(C n^{\omega(F) + \varepsilon}\) gates computes the product of every pair of \(n \times n\) matrices over \(F\).

theorem squareMatrixMultiplicationCircuitExponent_endpoint (F : Type u) [Field F]
    (hfinite : squareMatrixMultiplicationCircuitExponent F ≠ ⊤) :
    HasRectangularCircuitExponent F 1
      (squareMatrixMultiplicationCircuitExponent F).toReal

Uses 3

Statement usesAdmissible rectangular circuit exponents · Square matrix multiplication circuit exponent

Proof usesA finite rectangular circuit exponent is attained

30 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.