Empirical entropies of a finite population

Under the uniform measure on a finite type, conditional entropies are counts: each fibre of the conditioning attribute weighs in by its share of the population, with the entropy of the distribution of the other attribute on it. Equivalently the conditional entropy is an average over the population of the logarithm of the ratio of two class sizes, which needs no finite type of values.

References

• [CT06], chapter 2.

theorem InformationTheory.condEntropy_uniformOn_univ {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] [DecidableEq S] [MeasurableSpace T] [MeasurableSingletonClass T] [Fintype T] [DecidableEq T] (X : Ω → S) (Y : Ω → T) : condEntropy X Y (ProbabilityTheory.uniformOn Set.univ) = ∑ y : T, ↑{x : Ω | Y x = y}.card / ↑(Fintype.card Ω) * ∑ x : S, (↑{ω : Ω | Y ω = y ∧ X ω = x}.card / ↑{x : Ω | Y x = y}.card).negMulLog

The conditional entropy of one attribute of a finite population given another, under the uniform measure, weighs each fibre of Y by its share of the population and takes the entropy of the distribution of X on the fibre, all as counts.

theorem InformationTheory.condEntropy_uniformOn_univ_eq_sum_log {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSingletonClass S] [DecidableEq S] [MeasurableSpace T] [MeasurableSingletonClass T] [DecidableEq T] (X : Ω → S) (Y : Ω → T) : condEntropy X Y (ProbabilityTheory.uniformOn Set.univ) = (↑(Fintype.card Ω))⁻¹ * ∑ ω : Ω, Real.log (↑{x : Ω | Y x = Y ω}.card / ↑{ω' : Ω | Y ω' = Y ω ∧ X ω' = X ω}.card)

The conditional entropy of one attribute of a finite population given another, under the uniform measure, is the average over the population of the logarithm of the size of an individual's class under Y over the size of its class under Y and X together.