x y : ℝ
n : ℕ
⊢ Tendsto (fun x => log x ^ n / id x) atTop (𝓝 0)

x y : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
x y : ℝ
n : ℕ
⊢ (fun x => log x ^ n) =o[atTop] id
rw [Asymptotics.isLittleO_iff_tendsto']
no goals
x y : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim
no goals
x y : ℝ
n : ℕ
⊢ Tendsto (fun x => log x ^ n / id x) atTop (𝓝 0)
simpa using tendsto_pow_log_div_mul_add_atTop 1 0 n one_ne_zero