English
The derivative of sqrt x times log x is (2 + log x)/(2 sqrt x) for x ≠ 0; for x ≤ 0 the derivative is 0 in the appropriate sense.
Русский
Производная sqrt x умноженного на log x равна (2 + log x)/(2 sqrt x) при x ≠ 0; для x ≤ 0 производная равна 0 в подходящем смысле.
LaTeX
$$$x \neq 0 \implies \dfrac{d}{dx}(\sqrt x \log x) = \dfrac{2 + \log x}{2 \sqrt x}$$$
Lean4
theorem deriv_sqrt_mul_log (x : ℝ) : deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x) :=
by
rcases lt_or_ge 0 x with hx | hx
· exact (hasDerivAt_sqrt_mul_log hx.ne').deriv
· rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)
refine (hasDerivWithinAt_const x _ 0).congr_of_mem (fun x hx => ?_) hx
rw [sqrt_eq_zero_of_nonpos hx, zero_mul]
