qaryEntropy_pos

Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

English

If 0 < p < 1, then qaryEntropy q p > 0 for all q ∈ ℕ.

Русский

Если 0 < p < 1, то qaryEntropy q p > 0 для любого q ∈ ℕ.

LaTeX

$$$ 0 < p < 1 \Rightarrow qaryEntropy q p > 0 $$$

Lean4

theorem qaryEntropy_pos (hp₀ : 0 < p) (hp₁ : p < 1) : 0 < qaryEntropy q p :=
  by
  unfold qaryEntropy
  have := binEntropy_pos hp₀ hp₁
  positivity

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

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

Разделы

Аффилиация

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