ExponentComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Comparing power growth

The last scalar step of the auxiliary-separation argument compares a fourth-power lower bound for the cube of the diagonal profile with its dimension upper bound. Powers of two suffice to compare the exponents, so the argument needs no asymptotic estimates or approximation of constants.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.rpow_exponent_le_of_nat_bound line 19
Source documentation
A uniform bound on all positive natural inputs forces the exponent on the left to be no larger than the exponent on the right.
```
theorem rpow_exponent_le_of_nat_bound {a b C : ℝ}
    (hbound : ∀ n : ℕ, 1 ≤ n → (n : ℝ) ^ a ≤ C * (n : ℝ) ^ b) :
    a ≤ b := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.diagonal_exponent_le_three_quarters line 43

Source documentation

The diagonal lower bound and the dimension upper bound force the scalar exponent to be at most 3/4.

theorem diagonal_exponent_le_three_quarters {D : ℕ → ℝ} {t : ℝ}
    (ht : 0 < t)
    (hnonneg : ∀ n : ℕ, 1 ≤ n → 0 ≤ D n)
    (hlower : ∀ n : ℕ, 1 ≤ n → (n : ℝ) ^ 4 ≤ D n ^ 3)
    (hupper : ∀ n : ℕ, 1 ≤ n → D n ≤ (2 * (n : ℝ) - 1) ^ (1 / t)) :
    t ≤ 3 / 4 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.three_mul_diagonal_exponent_le_nine_quarters line 78

Source documentation

The scalar comparison in the normalization used for the matrix multiplication exponent.

theorem three_mul_diagonal_exponent_le_nine_quarters {D : ℕ → ℝ} {t : ℝ}
    (ht : 0 < t)
    (hnonneg : ∀ n : ℕ, 1 ≤ n → 0 ≤ D n)
    (hlower : ∀ n : ℕ, 1 ≤ n → (n : ℝ) ^ 4 ≤ D n ^ 3)
    (hupper : ∀ n : ℕ, 1 ≤ n → D n ≤ (2 * (n : ℝ) - 1) ^ (1 / t)) :
    3 * t ≤ 9 / 4 := by
…