hasDerivAt_sqrt_mul_log — Mathlib

English

If x ≠ 0, the derivative of x ↦ √x log x is (2 + log x)/(2√x).

Русский

Если x ≠ 0, производная функции x ↦ √x log x равна (2 + log x)/(2√x).

LaTeX

$$deriv (fun x => sqrt x * log x) x = (2 + log x)/(2*sqrt x)$$

Lean4

theorem hasDerivAt_sqrt_mul_log {x : ℝ} (hx : x ≠ 0) : HasDerivAt (fun x => √x * log x) ((2 + log x) / (2 * √x)) x :=
  by
  convert (hasDerivAt_sqrt hx).mul (hasDerivAt_log hx) using 1
  rw [add_div, div_mul_cancel_left₀ two_ne_zero, ← div_eq_mul_inv, sqrt_div_self', add_comm, one_div, one_div, ←
    div_eq_inv_mul]

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