deriv2_binEntropy

Mathlib.Analysis.SpecialFunctions.BinaryEntropy

URI: https://scilib.ai/kg/mathlib#Real.deriv2_binEntropy

English

The second derivative of binEntropy p with respect to p is -1/(p(1 − p)).

Русский

Вторая производная binEntropy по p равна −1/(p(1 − p)).

LaTeX

$$$ \mathrm{deriv}^{[2]} binEntropy p = -\dfrac{1}{p\,(1 - p)} $$$

Lean4

theorem deriv2_binEntropy : deriv^[2] binEntropy p = -1 / (p * (1 - p)) :=
  qaryEntropy_two ▸ deriv2_qaryEntropy

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

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

Разделы

Аффилиация

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