UpperSlope.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.loglog_le_of_power_bound line 10

Source documentation

A double logarithm estimate for the elementary denominator bound.

theorem loglog_le_of_power_bound {k : ℕ} {x : ℝ} (hk : 2 ≤ k)
    (hx : 2 ≤ x) (hbound : x ≤ 1 + (k : ℝ) ^ (2 ^ (k - 1))) :
    Real.log (Real.log x) ≤ (k : ℝ) * Real.log 2 + Real.log (Real.log k) := by
…

theorem OAI.Problem337.tendsto_log_nat_div_nat line 41
Source documentation
The logarithmic error in the denominator upper bound is negligible.
```
theorem tendsto_log_nat_div_nat :
    Tendsto (fun k : ℕ => Real.log (k : ℝ) / (k : ℝ)) atTop (𝓝 0) := by
…
```

theorem OAI.Problem337.power_bound_slope_limits line 47

Source documentation

The elementary power upper bound forces the sharp upper logarithmic slope.

theorem power_bound_slope_limits (u : ℕ → ℝ)
    (hu : ∀ᶠ k in atTop, 2 ≤ u k ∧
      u k ≤ 1 + (k : ℝ) ^ (2 ^ (k - 1))) :
    0 ≤ liminf (fun k => Real.log (Real.log (u k)) / (k : ℝ)) atTop ∧
    liminf (fun k => Real.log (Real.log (u k)) / (k : ℝ)) atTop ≤
      limsup (fun k => Real.log (Real.log (u k)) / (k : ℝ)) atTop ∧
    limsup (fun k => Real.log (Real.log (u k)) / (k : ℝ)) atTop ≤ Real.log 2 := by
…