Mutual information of a joint measure #
Mutual information is the Kullback-Leibler divergence of a joint measure from
the product of its marginals. It is reference-free — unlike entropy, it needs
no background measure — so it is stated at the level of measures; the discrete
PMF.mutualInformation is its toMeasure shadow
(PMF.mutualInformation_eq_toReal_mutualInfo). [UPSTREAM] candidate for
Mathlib/InformationTheory/, which has klDiv and Measure.fst/Measure.snd
but no mutual information.
noncomputable def
InformationTheory.mutualInfo
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(ρ : MeasureTheory.Measure (α × β))
:
ENNReal
Mutual information of a joint measure: its Kullback-Leibler divergence from the product of its marginals.
Equations
- InformationTheory.mutualInfo ρ = InformationTheory.klDiv ρ (ρ.fst.prod ρ.snd)