InformationTheory.Shannon.MutualInfoFiniteRange
Mutual information against a variable of finite range #
Mutual information is a divergence, so nothing bounds it in general. As soon as one of the two variables ranges over a finite alphabet, though, the information the pair shares is capped by the entropy of that variable alone, hence by the log of its alphabet size, and the bound does not see the other side at all: it may range over an arbitrary standard Borel space. Finiteness of the information is the same statement read qualitatively, and it is what lets the estimates be moved into the reals.
The degenerate end of the scale is a variable whose range is a single point up to a null set. Such a variable is independent of everything, so it shares no information with any other one, and conditioning on it is the same as not conditioning at all.
Main statements #
mutualInfo_ne_top_of_fintype_right— a finite alphabet on one side alone makes the mutual information finite.mutualInfo_le_ofReal_log_card— that mutual information is at most the log of the finite alphabet size.mutualInfo_eq_zero_of_ae_const— an almost everywhere constant variable shares no information.condMutualInfo_eq_mutualInfo_of_ae_const— conditioning on an almost everywhere constant variable leaves the mutual information unchanged.
InformationTheory.Shannon.mutualInfo_ne_top_of_fintype_right
source{Ω : Type u_1}
[MeasurableSpace Ω]
{A : Type u_2}
[MeasurableSpace A]
[StandardBorelSpace A]
[Nonempty A]
{B : Type u_3}
[Fintype B]
[Nonempty B]
[MeasurableSpace B]
[MeasurableSingletonClass B]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Ω → A)
(Yo : Ω → B)
(hXs : Measurable Xs)
(hYo : Measurable Yo)
:
Used by
InformationTheory.Shannon.mutualInfo_le_ofReal_log_card
source{Ω : Type u_1}
[MeasurableSpace Ω]
{A : Type u_2}
[MeasurableSpace A]
[StandardBorelSpace A]
[Nonempty A]
{B : Type u_3}
[Fintype B]
[Nonempty B]
[MeasurableSpace B]
[MeasurableSingletonClass B]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Ω → A)
(Yo : Ω → B)
(hXs : Measurable Xs)
(hYo : Measurable Yo)
:
Used by
InformationTheory.Shannon.mutualInfo_eq_zero_of_ae_const
source{Ω : Type u_1}
[MeasurableSpace Ω]
{A : Type u_2}
[MeasurableSpace A]
{B : Type u_3}
[MeasurableSpace B]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Ω → A)
(Yo : Ω → B)
(hYo : Measurable Yo)
(c : A)
(hc : Xs =ᵐ[μ] fun (x : Ω) => c)
:
Used by
InformationTheory.Shannon.condMutualInfo_eq_mutualInfo_of_ae_const
source{Ω : Type u_1}
{A : Type u_2}
{B : Type u_3}
{C : Type u_4}
[MeasurableSpace Ω]
[MeasurableSpace A]
[StandardBorelSpace A]
[Nonempty A]
[MeasurableSpace B]
[StandardBorelSpace B]
[Nonempty B]
[MeasurableSpace C]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Ω → A)
(Yo : Ω → B)
(Zc : Ω → C)
(hXs : Measurable Xs)
(hYo : Measurable Yo)
(hZc : Measurable Zc)
(c : C)
(hc : Zc =ᵐ[μ] fun (x : Ω) => c)
: