Theorems · Definition · information theory
Real.qaryEntropy
ℕ → ℝ → ℝ
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.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Real.logproof · cited by 939
- Real.binEntropyproof · cited by 28
Cited by18
Results whose statement or proof uses this declaration.
- Real.deriv_qaryEntropystatement · cited by 6
- Real.qaryEntropy_twostatement · cited by 4
- Real.qaryEntropy_continuousstatement · cited by 3
- Real.deriv2_qaryEntropystatement and proof · cited by 2
- Real.qaryEntropy_posstatement · cited by 1
- Real.qaryEntropy_strictAntiOnstatement · cited by 1
- Real.qaryEntropy_strictMonoOnstatement · cited by 1
- Real.qaryEntropy_zerostatement · cited by 1
- Real.strictConcaveOn_qaryEntropystatement · cited by 1
- Real.differentiableAt_qaryEntropystatement · cited by 1
- Real.qaryEntropy_onestatement · cited by 0
- Real.hasDerivAt_qaryEntropystatement · cited by 0