MI = 0 ↔ joint equals product of marginals #
Under absolute continuity of the joint with respect to the product of its marginals, and finite KL, MI vanishes iff the joint is the independent product. The finite-KL hypothesis is mathematically necessary for the forward direction: without it, a non-integrable log-likelihood ratio collapses the Bochner integral to 0 even when the measures differ.
theorem
InformationTheory.mutualInformationReal_eq_zero_iff_product
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(P : MeasureTheory.Measure (α × β))
[MeasureTheory.IsProbabilityMeasure P]
(hac : P.AbsolutelyContinuous ((MeasureTheory.Measure.map Prod.fst P).prod (MeasureTheory.Measure.map Prod.snd P)))
(hfin : klDiv P ((MeasureTheory.Measure.map Prod.fst P).prod (MeasureTheory.Measure.map Prod.snd P)) ≠ ⊤)
:
MI vanishes iff the joint is the product of its marginals, under absolute continuity and finite KL.