Asymptotics of log

Stream: Is there code for X?

[Arend Mellendijk]

Do we have some version of
example : (fun N:ℕ => Real.log (Real.log N)) =o[Filter.atTop] (fun N:ℕ => Real.log N)
or
example (ε:ℝ) (hε : ε > 0) : (fun N:ℕ => Real.log N) =O[Filter.atTop] fun N:ℕ => (N:ℝ)^ε?

With either one of these I'll be able to prove $\pi(N)\ll N/\log{N}$

[Yury G. Kudryashov]

You can use docs#Real.isLittleO_log_id_atTop_atTop with docs#Asymptotics.IsLittleO.comp_tendsto

[Yury G. Kudryashov]

(for the first one)

[Yury G. Kudryashov]

Or docs#isLittleO_log_rpow_atTop for the second one

[Arend Mellendijk]

Thank you! I had a feeling a bunch of asymptotic results were hidden somewhere.