deriv_sqrt_mul_log'

Mathlib.Analysis.Convex.SpecificFunctions.Deriv

URI: https://scilib.ai/kg/mathlib#deriv_sqrt_mul_log'

English

The function x ↦ √x log x is strictly concave on (1, ∞).

Русский

Функция x ↦ √x log x строго выпукла по конку (1, ∞).

LaTeX

$$StrictConcaveOn Real Set.Ioi 1 (fun x => sqrt x * log x)$$

Lean4

theorem deriv_sqrt_mul_log' : (deriv fun x => √x * log x) = fun x => (2 + log x) / (2 * √x) :=
  funext deriv_sqrt_mul_log

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru