binEntropy_strictAntiOn — Mathlib

English

Binary entropy is strictly decreasing on the interval [1/2, 1].

Русский

Бинарная энтропия строго убывает на отрезке [1/2, 1].

LaTeX

$$$ \text{StrictAntiOn}(binEntropy, \ Icc(2^{-1}, 1)) $$$

Lean4

/-- Binary entropy is strictly decreasing in interval [1/2, 1]. -/
theorem binEntropy_strictAntiOn : StrictAntiOn binEntropy (Icc 2⁻¹ 1) :=
  by
  rw [show (Icc (2⁻¹ : ℝ) 1) = Icc (1 / 2) 1 by norm_num, ← qaryEntropy_two]
  convert qaryEntropy_strictAntiOn (by rfl) using 1
  norm_num

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