deriv2_negMulLog — Mathlib

English

The second derivative of -x log x equals -1/x for x ≠ 0.

Русский

Вторая производная от −x log x равна −1/x при x ≠ 0.

LaTeX

$$$ \dfrac{d^2}{dx^2}(-x\log x) = -\dfrac{1}{x} \quad (x \neq 0). $$$

Lean4

theorem deriv2_negMulLog (x : ℝ) : deriv^[2] negMulLog x = -x⁻¹ :=
  by
  rw [negMulLog_eq_neg]
  have h := deriv2_mul_log
  simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp, deriv.fun_neg', Function.comp_apply] at h ⊢
  rw [h]

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