Removing polynomial overhead from exponential inequalities

The interpolation argument in Section 4 bounds tensor powers with an extra linear factor. Such a factor does not change their exponential growth rate. The statements below include eventual inequalities and constant factors, so the same argument also removes fixed counting losses in entropy limits.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.le_of_eventually_pow_le_linear_mul_pow {a b K C : ℝ} (ha : 0 ≤ a) (h : ∀ᶠ (j : ℕ) in Filter.atTop, b ^ j ≤ (↑j * K + C) * a ^ j) : b ≤ a

An eventual linear prefactor cannot increase an exponential growth rate.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.le_of_pow_le_linear_mul_pow {a b K : ℝ} (ha : 0 ≤ a) (h : ∀ (j : ℕ), b ^ j ≤ (↑j * K + 1) * a ^ j) : b ≤ a

Removing the linear interpolation overhead from inequalities for all powers.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.le_of_eventually_pow_le_const_mul_pow {a b C : ℝ} (ha : 0 ≤ a) (h : ∀ᶠ (j : ℕ) in Filter.atTop, b ^ j ≤ C * a ^ j) : b ≤ a

Fixed multiplicative losses disappear on taking exponential growth rates.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.le_of_pow_le_const_mul_pow {a b C : ℝ} (ha : 0 ≤ a) (h : ∀ (j : ℕ), b ^ j ≤ C * a ^ j) : b ≤ a

An all-powers form of constant-factor removal.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.le_of_pow_le_five_mul_pow {a b : ℝ} (ha : 0 ≤ a) (h : ∀ (j : ℕ), b ^ j ≤ 5 * a ^ j) : b ≤ a

In particular, the fixed factor five in the type-counting bound is harmless.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exp_le_of_tendsto_log_div {u : ℕ → ℝ} {n : ℕ → ℕ} {b C L : ℝ} (hb : 0 < b) (hC : 0 < C) (hn : Filter.Tendsto n Filter.atTop Filter.atTop) (hu : ∀ᶠ (k : ℕ) in Filter.atTop, 0 < u k) (hlim : Filter.Tendsto (fun (k : ℕ) => Real.log (u k) / ↑(n k)) Filter.atTop (nhds L)) (hbound : ∀ᶠ (k : ℕ) in Filter.atTop, u k ≤ C * b ^ n k) : Real.exp L ≤ b

A fixed counting loss does not contribute to a normalized logarithmic growth rate. The exponent may run through any sequence tending to infinity, including the multiples of a common denominator used for rational types.