Mutual information between two components of a joint distribution #
mutualInformationReal P = klDivReal P (P_A ⊗ P_B) where
P_A = P.map Prod.fst and P_B = P.map Prod.snd. ℝ-valued throughout,
so downstream linarith / nlinarith / field_simp work directly.
noncomputable def
InformationTheory.mutualInformationReal
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(P : MeasureTheory.Measure (α × β))
:
ℝ-valued mutual information of a joint measure.