RankExponent.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.exists_rankAtMost line 22
Source documentation
Every finite coefficient tensor has a finite exact rank decomposition.
```
theorem exists_rankAtMost {X Y Z : Type*} [Fintype X] [Fintype Y] [Fintype Z]
    (T : Tensor ℂ X Y Z) : ∃ r : ℕ, Tensor.RankAtMost T r := by
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.exactRank line 36
Source documentation
Exact rank of a finite complex coefficient tensor.
```
def exactRank {X Y Z : Type*} [Fintype X] [Fintype Y] [Fintype Z]
    (T : Tensor ℂ X Y Z) : ℕ := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRank_spec line 42
Source documentation
The least exact rank comes with an actual rank decomposition.
```
theorem exactRank_spec {X Y Z : Type*} [Fintype X] [Fintype Y] [Fintype Z]
    (T : Tensor ℂ X Y Z) : Tensor.RankAtMost T (exactRank T) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRank
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRank_le line 48
Source documentation
Every exact decomposition bounds the least rank.
```
theorem exactRank_le {X Y Z : Type*} [Fintype X] [Fintype Y] [Fintype Z]
    {T : Tensor ℂ X Y Z} {r : ℕ} (h : Tensor.RankAtMost T r) : exactRank T ≤ r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRank

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRank_restrict_le line 54

Source documentation

Exact rank cannot increase under a linear restriction.

theorem exactRank_restrict_le {X Y Z X' Y' Z' : Type*}
    [Fintype X] [Fintype Y] [Fintype Z]
    [Fintype X'] [Fintype Y'] [Fintype Z']
    (T : Tensor ℂ X Y Z) (A : X' → X → ℂ) (B : Y' → Y → ℂ)
    (C : Z' → Z → ℂ) : exactRank (Tensor.restrict A B C T) ≤ exactRank T :=
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRank

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRank_reindex line 62

Source documentation

Independent bijections of the three coordinate sets preserve exact rank.

theorem exactRank_reindex {X Y Z X' Y' Z' : Type*}
    [Fintype X] [Fintype Y] [Fintype Z]
    [Fintype X'] [Fintype Y'] [Fintype Z']
    (T : Tensor ℂ X Y Z) (ex : X' ≃ X) (ey : Y' ≃ Y) (ez : Z' ≃ Z) :
    exactRank (Tensor.pullback ex ey ez T) = exactRank T := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRank

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRank_product_le line 76

Source documentation

Tensor product decompositions give the usual submultiplicative rank bound.

theorem exactRank_product_le {X Y Z U V W : Type*}
    [Fintype X] [Fintype Y] [Fintype Z]
    [Fintype U] [Fintype V] [Fintype W]
    (T : Tensor ℂ X Y Z) (S : Tensor ℂ U V W) :
    exactRank (Tensor.product T S) ≤ exactRank T * exactRank S :=
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRank

def OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank line 84
Source documentation
Exact rank of the square matrix multiplication tensor.
```
def exactMatrixRank (n : ℕ) : ℕ := exactRank (Tensor.matrixMultiplication n n n)
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRank
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_spec line 86
theorem OAI.MatrixMultiplication.AuxiliarySeparation.matrixMultiplication_rankAtMost_cubic line 91
Source documentation
The ordinary scalar multiplication algorithm uses n³ simple tensors.
```
theorem matrixMultiplication_rankAtMost_cubic (n : ℕ) :
    Tensor.RankAtMost (Tensor.matrixMultiplication n n n) (n ^ 3) := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_upper line 110
theorem OAI.MatrixMultiplication.AuxiliarySeparation.matrixMultiplication_rank_lower line 114
Source documentation
An identity minor of the output flattening forces the quadratic lower bound.
```
theorem matrixMultiplication_rank_lower {n R : ℕ} (hn : 0 < n)
    (hRank : Tensor.RankAtMost (Tensor.matrixMultiplication n n n) R) : n ^ 2 ≤ R := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_lower line 127
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_pos line 130
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_zero line 133
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_one line 136
def OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponentSet line 142
Source documentation
The set of finite exact-rank exponents in the definition of ν.
```
def exactRankExponentSet : Set ℝ :=
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent line 146
Source documentation
The exact-rank exponent ν = inf_{n ≥ 2} log(R(Tₙ))/log(n).
```
def exactRankExponent : ℝ := sInf exactRankExponentSet
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponentSet
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponentSet_nonempty line 148
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_logb_lower line 151
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_logb_upper line 160
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponentSet_bddBelow line 169
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_lower line 174
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_le_logb line 179
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_upper line 183
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_rpow_lower line 188
Source documentation
Each matrix multiplication tensor has rank at least n^ν.
```
theorem exactMatrixRank_rpow_lower {n : ℕ} (hn : 2 ≤ n) :
    (n : ℝ) ^ exactRankExponent ≤ exactMatrixRank n := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent, OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank_rpow_lower_of_pos line 196
Source documentation
The rank lower bound includes the one-dimensional boundary case.
```
theorem exactMatrixRank_rpow_lower_of_pos {n : ℕ} (hn : 0 < n) :
    (n : ℝ) ^ exactRankExponent ≤ exactMatrixRank n := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent, OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_exactMatrixRank_lt_rpow line 204
Source documentation
A strict upper bound for the infimum is witnessed by an actual finite block.
```
theorem exists_exactMatrixRank_lt_rpow {τ : ℝ} (hτ : exactRankExponent < τ) :
    ∃ n : ℕ, 2 ≤ n ∧ (exactMatrixRank n : ℝ) < (n : ℝ) ^ τ := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent, OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_rankAtMost_of_exponent_slack line 215
Source documentation
Finite decompositions approximate the exact-rank exponent with any positive slack.
```
theorem exists_rankAtMost_of_exponent_slack {ε : ℝ} (hε : 0 < ε) :
    ∃ n R : ℕ, 2 ≤ n ∧ Tensor.RankAtMost (Tensor.matrixMultiplication n n n) R ∧
      (R : ℝ) ≤ (n : ℝ) ^ (exactRankExponent + ε) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent