binEntropy_pos — Mathlib

English

For any p, binEntropy p is strictly less than log 2 unless p = 1/2; more precisely, binEntropy p < log 2 iff p ≠ 1/2.

Русский

Для любого p бинарная энтропия меньше log 2, кроме случая p = 1/2; точнее: H(p) < log 2, если p ≠ 1/2.

LaTeX

$$$\mathrm{binEntropy}(p) < \log 2 \;\Longleftrightarrow\; p \neq \tfrac{1}{2}.$$$

Lean4

theorem binEntropy_pos (hp₀ : 0 < p) (hp₁ : p < 1) : 0 < binEntropy p :=
  by
  unfold binEntropy
  have : 0 < 1 - p := sub_pos.2 hp₁
  have : 0 < log p⁻¹ := log_pos <| (one_lt_inv₀ hp₀).2 hp₁
  have : 0 < log (1 - p)⁻¹ := log_pos <| (one_lt_inv₀ ‹_›).2 (sub_lt_self _ hp₀)
  positivity

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