Surprisal #
The surprisal, or information content, of a point under a measure is the negative logarithm of the mass of the point. The summand of Shannon entropy at a point is the mass of the point times its surprisal.
References #
- [CT06], chapter 2.
noncomputable def
InformationTheory.surprisal
{S : Type u_1}
[MeasurableSpace S]
(μ : MeasureTheory.Measure S)
(s : S)
:
ℝ
The surprisal of the point s under the measure μ.
Equations
- InformationTheory.surprisal μ s = -Real.log (μ.real {s})
Instances For
theorem
InformationTheory.negMulLog_measureReal_singleton
{S : Type u_1}
[MeasurableSpace S]
(μ : MeasureTheory.Measure S)
(s : S)
:
(μ.real {s}).negMulLog = μ.real {s} * surprisal μ s