English
If p < 0, then binEntropy(p) < 0.
Русский
Если p < 0, то H(p) < 0.
LaTeX
$$$p < 0 \Rightarrow \mathrm{binEntropy}(p) < 0$$$
Lean4
/-- Outside the usual range of `binEntropy`, it is negative. This is due to `log p = log |p|`. -/
theorem binEntropy_neg_of_neg (hp : p < 0) : binEntropy p < 0 :=
by
rw [binEntropy, log_inv, log_inv]
suffices -p * log p < (1 - p) * log (1 - p) by linarith
by_cases hp' : p < -1
· have : log p < log (1 - p) := by
rw [← log_neg_eq_log]
exact log_lt_log (Left.neg_pos_iff.mpr hp) (by linarith)
nlinarith [log_pos_of_lt_neg_one hp']
· have : -p * log p ≤ 0 := by
wlog h : -1 < p
· simp only [show p = -1 by linarith, log_neg_eq_log, log_one, le_refl, mul_zero]
· nlinarith [log_neg_of_lt_zero hp h]
nlinarith [(log_pos (by linarith) : 0 < log (1 - p))]
