qaryEntropy_neg_of_neg — Mathlib

English

If p ≤ 0, then qaryEntropy q p ≤ 0 for all q.

Русский

Если p ≤ 0, то qaryEntropy q p ≤ 0 для любого q.

LaTeX

$$$ p \le 0 \Rightarrow qaryEntropy q p \le 0 $$$

Lean4

/-- Outside the usual range of `qaryEntropy`, it is negative. This is due to `log p = log |p|`. -/
theorem qaryEntropy_neg_of_neg (hp : p < 0) : qaryEntropy q p < 0 :=
  add_neg_of_nonpos_of_neg (mul_nonpos_of_nonpos_of_nonneg hp.le (log_intCast_nonneg _)) (binEntropy_neg_of_neg hp)

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