Exact tensor rank and its matrix multiplication exponent

The rank is the least size of an exact decomposition into simple tensors. The exponent is the infimum of the finite matrix multiplication rank ratios from Section 3; no attainment of this real infimum is assumed.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_rankAtMost {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Finite X] [Finite Y] [Finite Z] (T : Foundation.Tensor K X Y Z) : ∃ (r : ℕ), T.RankAtMost r

Every finite coefficient tensor has a finite exact rank decomposition.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRank {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : ℕ

Exact rank of a finite coefficient tensor over K.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRank T = Nat.find ⋯

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRank_spec {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : T.RankAtMost (exactRank T)

The least exact rank comes with an actual rank decomposition.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRank_le {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} {r : ℕ} (h : T.RankAtMost r) : exactRank T ≤ r

Every exact decomposition bounds the least rank.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRank_restrict_le {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (T : Foundation.Tensor K X Y Z) (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) : exactRank (Foundation.Tensor.restrict A B C T) ≤ exactRank T

Exact rank cannot increase under a linear restriction.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRank_reindex {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (T : Foundation.Tensor K X Y Z) (ex : X' ≃ X) (ey : Y' ≃ Y) (ez : Z' ≃ Z) : exactRank (Foundation.Tensor.pullback (⇑ex) (⇑ey) (⇑ez) T) = exactRank T

Independent bijections of the three coordinate sets preserve exact rank.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRank_product_le {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : exactRank (T.product S) ≤ exactRank T * exactRank S

Tensor product decompositions give the usual submultiplicative rank bound.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank (K : Type) [Field K] (n : ℕ) : ℕ

Exact rank of the square matrix multiplication tensor.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_spec {K : Type} [Field K] (n : ℕ) : (Foundation.Tensor.matMul K n n n).RankAtMost (exactMatrixRank K n)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.matrixMultiplication_rankAtMost_cubic {K : Type} [Field K] (n : ℕ) : (Foundation.Tensor.matMul K n n n).RankAtMost (n ^ 3)

The ordinary scalar multiplication algorithm uses n³ simple tensors.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_upper {K : Type} [Field K] (n : ℕ) : exactMatrixRank K n ≤ n ^ 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.matrixMultiplication_rank_lower {K : Type} [Field K] {n R : ℕ} (hn : 0 < n) (hRank : (Foundation.Tensor.matMul K n n n).RankAtMost R) : n ^ 2 ≤ R

An identity minor of the output flattening forces the quadratic lower bound.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_lower {K : Type} [Field K] {n : ℕ} (hn : 0 < n) : n ^ 2 ≤ exactMatrixRank K n

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_pos {K : Type} [Field K] {n : ℕ} (hn : 0 < n) : 0 < exactMatrixRank K n

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_zero {K : Type} [Field K] : exactMatrixRank K 0 = 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_one {K : Type} [Field K] : exactMatrixRank K 1 = 1

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponentSet (K : Type) [Field K] : Set ℝ

The set of finite exact-rank exponents in the definition of ν.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponent (K : Type) [Field K] : ℝ

The exact-rank exponent ν = inf_{n ≥ 2} log(R(Tₙ))/log(n).

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponent K = sInf (MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponentSet K)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponentSet_nonempty {K : Type} [Field K] : (exactRankExponentSet K).Nonempty

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_logb_lower {K : Type} [Field K] {n : ℕ} (hn : 2 ≤ n) : 2 ≤ Real.logb ↑n ↑(exactMatrixRank K n)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_logb_upper {K : Type} [Field K] {n : ℕ} (hn : 2 ≤ n) : Real.logb ↑n ↑(exactMatrixRank K n) ≤ 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponentSet_bddBelow {K : Type} [Field K] : BddBelow (exactRankExponentSet K)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_lower {K : Type} [Field K] : 2 ≤ exactRankExponent K

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_le_logb {K : Type} [Field K] {n : ℕ} (hn : 2 ≤ n) : exactRankExponent K ≤ Real.logb ↑n ↑(exactMatrixRank K n)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_upper {K : Type} [Field K] : exactRankExponent K ≤ 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_rpow_lower {K : Type} [Field K] {n : ℕ} (hn : 2 ≤ n) : ↑n ^ exactRankExponent K ≤ ↑(exactMatrixRank K n)

Each matrix multiplication tensor has rank at least n^ν.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_rpow_lower_of_pos {K : Type} [Field K] {n : ℕ} (hn : 0 < n) : ↑n ^ exactRankExponent K ≤ ↑(exactMatrixRank K n)

The rank lower bound includes the one-dimensional boundary case.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_exactMatrixRank_lt_rpow {K : Type} [Field K] {τ : ℝ} (hτ : exactRankExponent K < τ) : ∃ (n : ℕ), 2 ≤ n ∧ ↑(exactMatrixRank K n) < ↑n ^ τ

A strict upper bound for the infimum is witnessed by an actual finite block.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_rankAtMost_of_exponent_slack {K : Type} [Field K] {ε : ℝ} (hε : 0 < ε) : ∃ (n : ℕ) (R : ℕ), 2 ≤ n ∧ (Foundation.Tensor.matMul K n n n).RankAtMost R ∧ ↑R ≤ ↑n ^ (exactRankExponent K + ε)

Finite decompositions approximate the exact-rank exponent with any positive slack.