tendsto_log

Stream: maths

[Jiale Miao]

Hi, I am wondering 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?

[Yaël Dillies]

I would get it by the fact that (x + 1)/x tends to 1 and log is continuous.

[Jiale Miao]

Sorry, I thought you misread the function? It is ‘log (x+1) / x’ instead of ‘log ((x+1)/x)’

[Sky Wilshaw]

You might find things like docs#asymptotics.is_o.rpow and docs#asymptotics.is_O.trans_is_o useful.

[Sky Wilshaw]

You might be able to use the lemma you found and compose it with some of these functions to get your result.

[Kevin Buzzard]

You want to understand $\frac{\log(k+1)}{k}$ but you understand $\frac{k}{k+1}$ so multiplying them together it suffices to understand $\frac{\log(k+1)}{k+1}$.