English
Shannon q-ary entropy of a random variable taking values in {1,...,q} with probability 1-p for outcome 1 and equal probability (p/(q-1)) for the remaining outcomes is given by qaryEntropy(q,p) = p log(q-1) + binEntropy(p).
Русский
Энтропия Шеннона для распределения q-ary: вероятности 1-p для исхода 1 и равные для остальных — p/(q-1); определение: qaryEntropy(q,p) = p log(q-1) + binEntropy(p).
LaTeX
$$$\mathrm{qaryEntropy}(q,p) = p \log (q - 1) + \mathrm{binEntropy}(p).$$$
Lean4
/-- Shannon q-ary Entropy function (measured in Nats, i.e., using natural logs).
It's the Shannon entropy of a random variable with possible outcomes {1, ..., q}
where outcome `1` has probability `1 - p` and all other outcomes are equally likely.
The usual domain of definition is p ∈ [0,1], i.e., input is a probability.
This is a generalization of the binary entropy function `binEntropy`. -/
@[pp_nodot]
noncomputable def qaryEntropy (q : ℕ) (p : ℝ) : ℝ :=
p * log (q - 1 : ℤ) + binEntropy p
