English
For all p, binEntropy p < log 2 iff p ≠ 1/2.
Русский
Для всех p: H(p) < log 2 тогда и только тогда, когда p ≠ 1/2.
LaTeX
$$$\mathrm{binEntropy}(p) < \log 2 \;\Leftrightarrow\; p \neq \tfrac{1}{2}$$$
Lean4
/-- For probability `p ≠ 0.5`, `binEntropy p < log 2`. -/
theorem binEntropy_lt_log_two : binEntropy p < log 2 ↔ p ≠ 2⁻¹ :=
by
refine ⟨?_, fun h ↦ ?_⟩
· rintro h rfl
simp at h
wlog hp : p < 2⁻¹
· have hp : 1 - p < 2⁻¹ := by rw [sub_lt_comm]; norm_num at *; linarith +splitNe
rw [← binEntropy_one_sub]
exact this hp.ne hp
obtain hp₀ | hp₀ := le_or_gt p 0
· exact (binEntropy_nonpos_of_nonpos hp₀).trans_lt <| log_pos <| by simp
have hp₁ : 0 < 1 - p := sub_pos.2 <| hp.trans <| by norm_num
calc
_ < log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) :=
strictConcaveOn_log_Ioi.2 (inv_pos.2 hp₀) (inv_pos.2 hp₁)
(by simpa [eq_sub_iff_add_eq, ← two_mul, mul_comm, mul_eq_one_iff_eq_inv₀]) hp₀ hp₁ (by simp)
_ = log 2 := by rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two] <;> positivity
