x_log_x_tendsto_atTop

x_log_x_tendsto_atTop.lean

-- TODO - upstream to mathlib
lemma x_log_x_tendsto_atTop: Filter.Tendsto ((fun x => x⁻¹) ∘ fun x => Real.log x / x) Filter.atTop Filter.atTop := by
  apply Filter.Tendsto.comp (f := fun x => Real.log x / x) (g := fun x => x⁻¹) (x := Filter.atTop) (y := (nhdsWithin 0 (Set.Ioi 0))) (z := Filter.atTop)
  .
    exact tendsto_inv_nhdsGT_zero (𝕜 := ℝ)
  .
    rw [tendsto_nhdsWithin_iff]
    refine ⟨?_, ?_⟩
    .
      have log_div_x := Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 (by simp)
      simp only [pow_one, one_mul, add_zero] at log_div_x
      exact log_div_x
    . simp only [Set.mem_Ioi, eventually_atTop, ge_iff_le]
      use 2
      intro x hx
      have log_pos: 0 < Real.log x := by
        refine (Real.log_pos_iff ?_).mpr ?_ <;> linarith
      positivity