English
For x ≠ 0, the second derivative of f(x) = x log x satisfies f''(x) = 1/x.
Русский
Для x ≠ 0 вторaя производная f(x) = x log x равна f''(x) = 1/x.
LaTeX
$$$\dfrac{d^2}{dx^2}\bigl(x \log x\bigr) = \dfrac{1}{x} \quad (x \neq 0)$$$
Lean4
theorem deriv2_mul_log (x : ℝ) : deriv^[2] (fun x ↦ x * log x) x = x⁻¹ :=
by
simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp, Function.comp_apply]
by_cases hx : x = 0
· rw [hx, inv_zero]
exact deriv_zero_of_not_differentiableAt (fun h ↦ not_continuousAt_deriv_mul_log_zero h.continuousAt)
· suffices ∀ᶠ y in (𝓝 x), deriv (fun x ↦ x * log x) y = log y + 1
by
refine (Filter.EventuallyEq.deriv_eq this).trans ?_
rw [deriv_add_const, deriv_log x]
filter_upwards [eventually_ne_nhds hx] with y hy using deriv_mul_log hy
