tendsto_rightDeriv_mul_log_atTop — Mathlib

English

The right derivative of f(x) = x log x tends to +∞ as x → ∞.

Русский

Правая производная функции f(x) = x log x стремится к +∞ при x → ∞.

LaTeX

$$$\lim_{x \to \infty} \frac{d}{dx}\big|_{(I^{+}_{x})} (x \log x) = \infty$$$

Lean4

theorem tendsto_rightDeriv_mul_log_atTop :
    Tendsto (fun x ↦ derivWithin (fun x ↦ x * log x) (Set.Ioi x) x) atTop atTop :=
  by
  refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))
  rw [EventuallyEq, eventually_atTop]
  exact ⟨1, fun _ hx ↦ rightDeriv_mul_log (zero_lt_one.trans_le hx).ne'⟩

Похожие утверждения