PolynomialOverhead.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.le_of_eventually_pow_le_linear_mul_pow line 22
Source documentation
An eventual linear prefactor cannot increase an exponential growth rate.
```
theorem le_of_eventually_pow_le_linear_mul_pow {a b K C : ℝ}
    (ha : 0 ≤ a)
    (h : ∀ᶠ j : ℕ in atTop, b ^ j ≤ ((j : ℝ) * K + C) * a ^ j) :
    b ≤ a := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.le_of_pow_le_linear_mul_pow line 47
Source documentation
Removing the linear interpolation overhead from inequalities for all powers.
```
theorem le_of_pow_le_linear_mul_pow {a b K : ℝ} (ha : 0 ≤ a)
    (h : ∀ j : ℕ, b ^ j ≤ ((j : ℝ) * K + 1) * a ^ j) : b ≤ a :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.le_of_eventually_pow_le_const_mul_pow line 52
Source documentation
Fixed multiplicative losses disappear on taking exponential growth rates.
```
theorem le_of_eventually_pow_le_const_mul_pow {a b C : ℝ} (ha : 0 ≤ a)
    (h : ∀ᶠ j : ℕ in atTop, b ^ j ≤ C * a ^ j) : b ≤ a := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.le_of_pow_le_const_mul_pow line 58
Source documentation
An all-powers form of constant-factor removal.
```
theorem le_of_pow_le_const_mul_pow {a b C : ℝ} (ha : 0 ≤ a)
    (h : ∀ j : ℕ, b ^ j ≤ C * a ^ j) : b ≤ a :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.le_of_pow_le_five_mul_pow line 63
Source documentation
In particular, the fixed factor five in the type-counting bound is harmless.
```
theorem le_of_pow_le_five_mul_pow {a b : ℝ} (ha : 0 ≤ a)
    (h : ∀ j : ℕ, b ^ j ≤ 5 * a ^ j) : b ≤ a :=
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exp_le_of_tendsto_log_div line 70

Source documentation

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.

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