InformationTheory.Shannon.CondMutualInfoMixture
Averaging an information slot over a countable mixture #
A mixture of laws indexed by a countable tag is a composition product of the tag law with the kernel of the components, so the tag-conditioned mutual information of the mixture is the tag average of the mutual informations of the components. Adding back the tag term of the chain rule turns that into an identity for the mutual information of the mixture itself, whenever the variable in question recovers the tag; since that term is nonnegative, the identity also bounds the tag average of the components by the mutual information of the mixture.
None of the statements mentions a channel or a code: they are properties of mutualInfo and
condMutualInfo under a composition product of a countably supported measure with a Markov
kernel.
Main statements #
condMutualInfo_compProd_fst_eq_lintegralandcondMutualInfo_compProd_snd_eq_lintegral— the tag-conditioned mutual information of a mixture is the tag average of the components, in the unconditional and in the conditional form.mutualInfo_compProd_eq_add_lintegral— for a variable that recovers the tag, the mutual information of the mixture itself splits into the information the tag carries and the tag average of the components.
InformationTheory.Shannon.condMutualInfo_compProd_fst_eq_lintegral
source{T : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
[MeasurableSpace T]
[MeasurableSpace S]
[MeasurableSpace A]
[StandardBorelSpace A]
[Nonempty A]
[MeasurableSpace B]
[StandardBorelSpace B]
[Nonempty B]
[Countable T]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
(κ : ProbabilityTheory.Kernel T S)
[ProbabilityTheory.IsMarkovKernel κ]
{f : S → A}
{g : S → B}
(hf : Measurable f)
(hg : Measurable g)
:
condMutualInfo (μ.compProd κ) (fun (p : T × S) => f p.2) (fun (p : T × S) => g p.2) Prod.fst = ∫⁻ (t : T), mutualInfo (κ t) f g ∂μ
Used by
InformationTheory.Shannon.mutualInfo_compProd_eq_add_lintegral
source{T : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
[MeasurableSpace T]
[MeasurableSpace S]
[MeasurableSpace A]
[StandardBorelSpace A]
[Nonempty A]
[MeasurableSpace B]
[StandardBorelSpace B]
[Nonempty B]
[Countable T]
[MeasurableSingletonClass T]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
(κ : ProbabilityTheory.Kernel T S)
[ProbabilityTheory.IsMarkovKernel κ]
{f : S → A}
{g : S → B}
(hf : Measurable f)
(hg : Measurable g)
{tag : A → T}
(htag : Measurable tag)
(hrec : ∀ᵐ (p : T × S) ∂μ.compProd κ, tag (f p.2) = p.1)
:
(mutualInfo (μ.compProd κ) (fun (p : T × S) => f p.2) fun (p : T × S) => g p.2) = (mutualInfo (μ.compProd κ) Prod.fst fun (p : T × S) => g p.2) + ∫⁻ (t : T), mutualInfo (κ t) f g ∂μ
Used by
InformationTheory.Shannon.condMutualInfo_compProd_snd_eq_lintegral
source{T : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
[MeasurableSpace T]
[MeasurableSpace S]
[MeasurableSpace A]
[StandardBorelSpace A]
[Nonempty A]
[MeasurableSpace B]
[StandardBorelSpace B]
[Nonempty B]
[Countable T]
[MeasurableSingletonClass T]
{C : Type u_5}
[MeasurableSpace C]
[StandardBorelSpace C]
[Nonempty C]
(μ : MeasureTheory.Measure T)
[MeasureTheory.IsProbabilityMeasure μ]
(κ : ProbabilityTheory.Kernel T S)
[ProbabilityTheory.IsMarkovKernel κ]
{f : S → A}
{g : S → B}
{h : S → C}
(hf : Measurable f)
(hg : Measurable g)
(hh : Measurable h)
{tag : C → T}
(htag : Measurable tag)
(hrec : ∀ᵐ (p : T × S) ∂μ.compProd κ, tag (h p.2) = p.1)
(htagfin : (mutualInfo (μ.compProd κ) Prod.fst fun (p : T × S) => g p.2) ≠ ⊤)
(hmargfin : ∫⁻ (t : T), mutualInfo (κ t) h g ∂μ ≠ ⊤)
:
(condMutualInfo (μ.compProd κ) (fun (p : T × S) => f p.2) (fun (p : T × S) => g p.2) fun (p : T × S) => h p.2) = ∫⁻ (t : T), condMutualInfo (κ t) f g h ∂μ