Entropy and surprisal

Entropy is expected surprisal, and the expected surprisal under another measure, the cross-entropy, exceeds it by the Kullback–Leibler divergence. The exponential of minus each is a geometric mean of masses, of a measure's own masses for entropy and of the other measure's for cross-entropy.

References

• [CT06], chapter 2.

theorem InformationTheory.geomMean_eq_exp_neg_measureEntropy {S : Type u_1} [MeasurableSpace S] [Fintype S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] : (μ.geomMean fun (s : S) => μ {s}) = ENNReal.ofReal (Real.exp (-measureEntropy μ))

The geometric mean of the masses of a probability measure under itself is the exponential of minus its entropy.

theorem InformationTheory.measureEntropy_eq_tsum_mul_surprisal {S : Type u_1} [MeasurableSpace S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : measureEntropy μ = ∑' (s : S), μ.real {s} * (surprisal μ s).toReal

Entropy is expected surprisal; an atom of mass zero, whose surprisal is ∞, contributes 0 through its real part.

theorem InformationTheory.measureEntropy_eq_integral_surprisal {S : Type u_1} [MeasurableSpace S] [Countable S] [MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (h : MeasureTheory.Integrable (fun (s : S) => (surprisal μ s).toReal) μ) : measureEntropy μ = ∫ (s : S), (surprisal μ s).toReal ∂μ

theorem InformationTheory.lintegral_surprisal_eq_ofReal_add_klDiv {S : Type u_1} [MeasurableSpace S] {μ : MeasureTheory.Measure S} [MeasurableSingletonClass S] [Fintype S] {ν : MeasureTheory.Measure S} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsZeroOrProbabilityMeasure ν] : ∫⁻ (s : S), surprisal ν s ∂μ = ENNReal.ofReal (measureEntropy μ) + klDiv μ ν

The cross-entropy, the expected surprisal under μ of the atoms as ν weighs them, is the entropy of μ plus the divergence of μ from ν; both sides are infinite unless μ ≪ ν.

theorem InformationTheory.geomMean_eq_exp_neg_lintegral_surprisal {S : Type u_1} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] (μ ν : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsZeroOrProbabilityMeasure ν] : (μ.geomMean fun (s : S) => ν {s}) = (-↑(∫⁻ (s : S), surprisal ν s ∂μ)).exp

The geometric mean under μ of the masses of a probability measure ν is the exponential of minus the cross-entropy, the expected surprisal under μ of the atoms as ν weighs them.