Removing positive slack from the spectral inequality

The positive slack in the exponent can be sent to zero with the matrix size fixed. A bound at all positive natural sizes then removes a fixed additive error term.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.spectral_bound_of_positive_slack {ν k D : ℝ} {d n : ℕ} (hν : 0 < ν) (hn : 1 ≤ n) (hbound : ∀ (δ : ℝ), 0 < δ → ↑d ^ ν * ↑n ^ (ν / (ν + δ)) ≤ ↑n * k + D) : ↑d ^ ν * ↑n ≤ ↑n * k + D

Continuity removes the positive slack in the spectral exponent.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.coefficient_le_of_nat_mul_bound {a k D : ℝ} (hbound : ∀ (n : ℕ), 1 ≤ n → a * ↑n ≤ ↑n * k + D) : a ≤ k

A fixed additive error cannot enlarge a coefficient bounded at every positive natural size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.spectral_coefficient_le_of_all_nat {ν k D : ℝ} {d : ℕ} (hν : 0 < ν) (hbound : ∀ (n : ℕ), 1 ≤ n → ∀ (δ : ℝ), 0 < δ → ↑d ^ ν * ↑n ^ (ν / (ν + δ)) ≤ ↑n * k + D) : ↑d ^ ν ≤ k

Uniform spectral inequalities for all positive sizes and all positive slacks force the desired coefficient bound.