Growth.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QuantitativeVanDerWaerden.natLog_two_eq_floor_log line 16
Source documentation
The integer logarithm in the product construction is the floor of the real base-two logarithm.
```
theorem natLog_two_eq_floor_log (r : ℕ) :
    Nat.log 2 r = ⌊Real.log (r : ℝ) / Real.log 2⌋₊ := by
…
```
theorem OAI.QuantitativeVanDerWaerden.log_div_two_log_two_le_natLog line 21
Source documentation
A uniform lower estimate for the number of usable binary digits.
```
theorem log_div_two_log_two_le_natLog {r : ℕ} (hr : 2 ≤ r) :
    Real.log (r : ℝ) / (2 * Real.log 2) ≤ (Nat.log 2 r : ℝ) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.tendsto_kthRoot_of_eventually_rpow_bound line 37
Source documentation
A bound of the form k^(a*k) with positive fixed a forces the full kth-root limit, with no subsequence restriction.
```
theorem tendsto_kthRoot_of_eventually_rpow_bound
    {F : ℕ → ℝ} {a : ℝ} (ha : 0 < a)
    (h : ∀ᶠ k : ℕ in atTop, (k : ℝ) ^ (a * k) ≤ F k) :
    Tendsto (fun k : ℕ => (F k) ^ (1 / (k : ℝ))) atTop atTop := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.F