binEntropy — Mathlib

English

For p ∈ ℝ, binEntropy(p) = - p log p - (1-p) log(1-p); this is the Shannon entropy of a Bernoulli random variable with success probability p.

Русский

Для p ∈ ℝ функция binEntropy(p) равна - p log p - (1-p) log(1-p); это энтропия Бернулли с вероятностью успеха p.

LaTeX

$$$\mathrm{binEntropy}(p) = - p \log p - (1-p) \log (1-p).$$$

Lean4

/-- The [binary entropy function](https://en.wikipedia.org/wiki/Binary_entropy_function)
`binEntropy p := - p * log p - (1-p) * log (1 - p)`
is the Shannon entropy of a Bernoulli random variable with success probability `p`. -/
@[pp_nodot]
noncomputable def binEntropy (p : ℝ) : ℝ :=
  p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

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