English
The second derivative of sqrt x log x equals -log x /(4 sqrt x^3) for x > 0 (with appropriate handling for x ≤ 0).
Русский
Вторая производная функций sqrt x log x равна -log x /(4 sqrt x^3) при x>0 (для x≤0 — в корректном смысле нули).
LaTeX
$$deriv^[2] (fun x => sqrt x * log x) x = - log x / (4 * sqrt x ^ 3)$$
Lean4
theorem deriv2_sqrt_mul_log (x : ℝ) : deriv^[2] (fun x => √x * log x) x = -log x / (4 * √x ^ 3) :=
by
simp only [Nat.iterate, deriv_sqrt_mul_log']
rcases le_or_gt x 0 with hx | hx
· rw [sqrt_eq_zero_of_nonpos hx, zero_pow three_ne_zero, mul_zero, div_zero]
refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)
refine (hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => ?_) hx
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
· have h₀ : √x ≠ 0 := sqrt_ne_zero'.2 hx
convert
(((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <|
mul_ne_zero two_ne_zero h₀).deriv using
1
nth_rw 3 [← mul_self_sqrt hx.le]
generalize √x = sqx at h₀
field_simp
ring
