Exponent.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

From exact tensor rank to arithmetic complexity

This file supplies the arithmetic conversion in Section 6.2. It uses the existing division-free straight-line programs over ℂ: loading inputs and constants is free, and each scalar addition, subtraction, or multiplication costs one. Correctness means matrix multiplication on every pair of inputs.

The substantive tensor estimates are separate. Here omega is an alias for the existing arithmetic exponent, and the general bridge proves omega ≤ exactRankExponent. Thus any independently established upper bound on the exact-rank exponent gives an arithmetic bound with every positive exponent slack. No particular numerical upper bound is assumed or asserted.

abbrev OAI.MatrixMultiplication.AuxiliarySeparation.omega line 31
Source documentation
The arithmetic matrix multiplication exponent over the complex numbers, in the repository's existing scalar-operation model.
```
abbrev omega : ℝ := MatrixMultiplication.Arithmetic.omega ℂ
```
Mentions: OAI.MatrixMultiplication.Arithmetic.omega
abbrev OAI.MatrixMultiplication.AuxiliarySeparation.ArithmeticBound line 34
Source documentation
A uniform scalar-operation bound with arbitrary positive exponent slack.
```
abbrev ArithmeticBound (τ : ℝ) : Prop :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.arithmeticBound_iff_omega_le line 39
Source documentation
The existing arithmetic exponent is itself admissible; hence its infimum has exactly the expected upper-bound interpretation.
```
theorem arithmeticBound_iff_omega_le {τ : ℝ} :
    ArithmeticBound τ ↔ omega ≤ τ :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.ArithmeticBound, OAI.MatrixMultiplication.AuxiliarySeparation.omega
theorem OAI.MatrixMultiplication.AuxiliarySeparation.arithmeticComplexity_iff_omega_le line 45
Source documentation
Expanded form of the arithmetic statement, including its quantifier order and the correctness and operation cost of the resulting programs.
```
theorem arithmeticComplexity_iff_omega_le {τ : ℝ} :
    (∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧
      ∀ n : ℕ, 1 ≤ n →
        ∃ P : MatrixMultiplication.Arithmetic.MatrixAlgorithm ℂ n n n,
          P.Correct ∧ (P.cost : ℝ) ≤ C * (n : ℝ) ^ (τ + ε)) ↔ omega ≤ τ :=
…
```
Mentions: OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm, OAI.MatrixMultiplication.AuxiliarySeparation.omega
theorem OAI.MatrixMultiplication.AuxiliarySeparation.arithmeticBound_of_rankAtMost line 55
Source documentation
A finite exact decomposition gives an arithmetic bound by block substitution, including all the scalar operations in the linear combinations, followed by padding to arbitrary positive sizes.
```
theorem arithmeticBound_of_rankAtMost {n R : ℕ} (hn : 2 ≤ n)
    (hRank : Tensor.RankAtMost (Tensor.matrixMultiplication n n n) R)
    {τ : ℝ} (hτ : 2 ≤ τ) (hR : (R : ℝ) ≤ (n : ℝ) ^ τ) :
    ArithmeticBound τ :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.ArithmeticBound
theorem OAI.MatrixMultiplication.AuxiliarySeparation.omega_le_of_rankAtMost line 62
theorem OAI.MatrixMultiplication.AuxiliarySeparation.omega_le_logb_rank line 70
Source documentation
The quadratic rank lower bound pays for the quadratic block-combination overhead, including the boundary case of rank exactly n².
```
theorem omega_le_logb_rank {n R : ℕ} (hn : 2 ≤ n)
    (hRank : Tensor.RankAtMost (Tensor.matrixMultiplication n n n) R) :
    omega ≤ Real.logb (n : ℝ) (R : ℝ) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.omega
theorem OAI.MatrixMultiplication.AuxiliarySeparation.arithmeticBound_of_arbitrarily_close_rankBounds line 88
Source documentation
Near-optimal finite blocks suffice: no finite decomposition is required to attain the limiting exponent.
```
theorem arithmeticBound_of_arbitrarily_close_rankBounds {τ : ℝ} (hτ : 2 ≤ τ)
    (hRank : ∀ δ : ℝ, 0 < δ → ∃ n R : ℕ, 2 ≤ n ∧
      Tensor.RankAtMost (Tensor.matrixMultiplication n n n) R ∧
        (R : ℝ) ≤ (n : ℝ) ^ (τ + δ)) : ArithmeticBound τ := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.ArithmeticBound
theorem OAI.MatrixMultiplication.AuxiliarySeparation.omega_le_exactMatrixRank_logb line 99
Source documentation
The arithmetic exponent is bounded by each exact finite-block exponent.
```
theorem omega_le_exactMatrixRank_logb {n : ℕ} (hn : 2 ≤ n) :
    omega ≤ Real.logb (n : ℝ) (exactMatrixRank n : ℝ) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.omega, OAI.MatrixMultiplication.AuxiliarySeparation.exactMatrixRank
theorem OAI.MatrixMultiplication.AuxiliarySeparation.omega_le_exactRankExponent line 105
Source documentation
General exact-rank-to-arithmetic bridge. The proof uses a lower bound for every finite-block exponent, so it does not require attainment of the infimum.
```
theorem omega_le_exactRankExponent : omega ≤ exactRankExponent := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.omega, OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent
theorem OAI.MatrixMultiplication.AuxiliarySeparation.arithmeticBound_exactRankExponent line 110
theorem OAI.MatrixMultiplication.AuxiliarySeparation.arithmeticBound_of_exactRankExponent_le line 115
Source documentation
Any upper bound on the exact-rank exponent gives the same arithmetic exponent bound, with arbitrary positive slack.
```
theorem arithmeticBound_of_exactRankExponent_le {τ : ℝ}
    (hτ : exactRankExponent ≤ τ) : ArithmeticBound τ :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent, OAI.MatrixMultiplication.AuxiliarySeparation.ArithmeticBound

theorem OAI.MatrixMultiplication.AuxiliarySeparation.arithmeticComplexity_of_exactRankExponent_le line 120

Source documentation

Explicit epsilon-complexity conclusion from an exact-rank exponent bound.

theorem arithmeticComplexity_of_exactRankExponent_le {τ : ℝ}
    (hτ : exactRankExponent ≤ τ) (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 1 ≤ n →
      ∃ P : MatrixMultiplication.Arithmetic.MatrixAlgorithm ℂ n n n,
        P.Correct ∧ (P.cost : ℝ) ≤ C * (n : ℝ) ^ (τ + ε) :=
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent, OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm