binEntropy_two_inv

Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

English

For p = 1/2, binEntropy(p) = log 2.

Русский

Для p = 1/2, binEntropy(p) = log 2.

LaTeX

$$$\mathrm{binEntropy}\left(\tfrac{1}{2}\right) = \log 2$$$

Lean4

@[simp]
theorem binEntropy_two_inv : binEntropy 2⁻¹ = log 2 := by norm_num [binEntropy]; simp; ring

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

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

Разделы

Аффилиация

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