qaryEntropy_nonneg — Mathlib

English

If 0 ≤ p ≤ 1, then qaryEntropy q p ≥ 0 for all q ∈ ℕ.

Русский

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

LaTeX

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

Lean4

theorem qaryEntropy_nonneg (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : 0 ≤ qaryEntropy q p :=
  by
  obtain rfl | hp₀ := hp₀.eq_or_lt
  · simp
  obtain rfl | hp₁ := hp₁.eq_or_lt
  · simpa [qaryEntropy, -Int.cast_sub] using log_intCast_nonneg _
  exact (qaryEntropy_pos hp₀ hp₁).le

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