tendsto_log

Stream: general

[Jiale Miao]

What would be a good way to get proof of this?
tendsto (λ (k : ℕ), real.log (↑k + 1) / ↑k) at_top (nhds 0)
Since log goes slower than x, this is clearly true here. And I found this lemma in the mathlib which might be useful :

lemma is_o_log_rpow_rpow_at_top {s : ℝ} (r : ℝ) (hs : 0 < s) :
  (λ x, log x ^ r) =o[at_top] (λ x, x ^ s) :=

But I think what I may want is this version:

lemma name : (λ x, log (x + 1) ^ r) =o[at_top] (λ x, x ^ s) :=

Is there any suggestion here?

[Eric Wieser]

Probably best to stick to one topic and use https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/tendsto_log/near/314436804