binEntropy_two_inv_add — Mathlib

English

Binary entropy is symmetric about 1/2: binEntropy(1/2 + p) = binEntropy(1/2 - p).

Русский

Бинарная энтропия симметрична вокруг 1/2: H(1/2 + p) = H(1/2 - p).

LaTeX

$$$\mathrm{binEntropy}\left(\tfrac{1}{2} + p\right) = \mathrm{binEntropy}\left(\tfrac{1}{2} - p\right).$$$

Lean4

/-- `binEntropy` is symmetric about 1/2. -/
theorem binEntropy_two_inv_add (p : ℝ) : binEntropy (2⁻¹ + p) = binEntropy (2⁻¹ - p) := by rw [← binEntropy_one_sub];
  ring_nf

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