Nonnegativity of mutual information #
Delegates to klDivReal_nonneg after establishing that the product of
marginals of a probability measure is itself a probability measure.
theorem
InformationTheory.mutualInformationReal_nonneg
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(P : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure P]
:
Mutual information is nonnegative for probability measures.