binEntropy_strictMonoOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Binary entropy is strictly increasing in interval [0, 1/2]. -/
theorem binEntropy_strictMonoOn : StrictMonoOn binEntropy (Icc 0 2⁻¹) :=
  by
  rw [show Icc (0 : ℝ) 2⁻¹ = Icc 0 (1 - 1 / 2) by norm_num, ← qaryEntropy_two]
  exact qaryEntropy_strictMonoOn (by rfl)

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