InformationTheory.Shannon.MutualInfo
Mutual information via KL divergence #
mutualInfo μ X Y := klDiv (μ.map (X, Y)) ((μ.map X).prod (μ.map Y)) and its basic properties.
Main definitions #
mutualInfo—I(X; Y) := KL(P_{X,Y} ‖ P_X ⊗ P_Y).
Main statements #
mutualInfo_nonneg—0 ≤ I(X; Y).mutualInfo_comm—I(X; Y) = I(Y; X).mutualInfo_eq_zero_iff_indep—I(X; Y) = 0 ↔ X ⊥ Y.mutualInfo_ne_top—I(X; Y) ≠ ∞for finite alphabets.
InformationTheory.Shannon.mutualInfo
source{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Type u_2}
[MeasurableSpace X]
{Y : Type u_3}
[MeasurableSpace Y]
(μ : MeasureTheory.Measure Ω)
(Xs : Ω → X)
(Yo : Ω → Y)
:
Mutual information via KL divergence:
I(X; Y) := KL(P_{X,Y} ‖ P_X ⊗ P_Y).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.mutualInfo_nonneg
source{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Type u_2}
[MeasurableSpace X]
{Y : Type u_3}
[MeasurableSpace Y]
(μ : MeasureTheory.Measure Ω)
(Xs : Ω → X)
(Yo : Ω → Y)
:
Mutual information is nonneg (immediate from klDiv : ℝ≥0∞).
Used by
InformationTheory.Shannon.mutualInfo_congr_pair
source{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Type u_2}
[MeasurableSpace X]
{Y : Type u_3}
[MeasurableSpace Y]
{Ω' : Type u_4}
[MeasurableSpace Ω']
(μ : MeasureTheory.Measure Ω)
(μ' : MeasureTheory.Measure Ω')
{Xs : Ω → X}
{Yo : Ω → Y}
{Xs' : Ω' → X}
{Yo' : Ω' → Y}
(hXs : Measurable Xs)
(hYo : Measurable Yo)
(hXs' : Measurable Xs')
(hYo' : Measurable Yo')
(h :
MeasureTheory.Measure.map (fun (ω : Ω) => (Xs ω, Yo ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω') => (Xs' ω, Yo' ω)) μ')
:
Used by
InformationTheory.Shannon.klDiv_map_measurableEquiv
source{α : Type u_4}
{β : Type u_5}
[MeasurableSpace α]
[MeasurableSpace β]
(e : α ≃ᵐ β)
(μ ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
KL divergence is invariant under pushforward by a MeasurableEquiv.
Used by
InformationTheory.Shannon.klDiv_prod_const_left
source{α : Type u_4}
{β : Type u_5}
[MeasurableSpace α]
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsProbabilityMeasure μ]
(ν₁ ν₂ : MeasureTheory.Measure β)
[MeasureTheory.IsFiniteMeasure ν₁]
[MeasureTheory.IsFiniteMeasure ν₂]
:
klDiv (μ.prod ν₁) (μ.prod ν₂) = klDiv ν₁ ν₂ when μ is a probability measure.
Used by
InformationTheory.Shannon.mutualInfo_comm
source{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Type u_2}
[MeasurableSpace X]
{Y : Type u_3}
[MeasurableSpace Y]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(Xs : Ω → X)
(Yo : Ω → Y)
(hXs : Measurable Xs)
(hYo : Measurable Yo)
:
Mutual information is symmetric: I(X; Y) = I(Y; X).
Used by
InformationTheory.Shannon.mutualInfo_eq_zero_iff_indep
source{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Type u_2}
[MeasurableSpace X]
{Y : Type u_3}
[MeasurableSpace Y]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Ω → X)
(Yo : Ω → Y)
(hXs : Measurable Xs)
(hYo : Measurable Yo)
:
I(X; Y) = 0 ↔ X and Y are independent.
Used by
InformationTheory.Shannon.mutualInfo_ne_top
source{Ω : Type u_1}
[MeasurableSpace Ω]
{X : Type u_2}
[MeasurableSpace X]
{Y : Type u_3}
[MeasurableSpace Y]
[Fintype X]
[MeasurableSingletonClass X]
[Fintype Y]
[MeasurableSingletonClass Y]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Ω → X)
(Yo : Ω → Y)
(hXs : Measurable Xs)
(hYo : Measurable Yo)
:
Mutual information is finite for finite alphabets.