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 MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.rpow_exponent_le_of_nat_bound {a b C : ℝ} (hbound : ∀ (n : ℕ), 1 ≤ n → ↑n ^ a ≤ C * ↑n ^ b) : a ≤ b

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 MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

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