Data-processing inequality

TheoremSymmetry of mutual information#✓fully proved

I(Y; X) = I(X; Y).

theorem measureMutualInformation_map_swap (μ : ProbabilityMeasure (X × Y)) :
    measureMutualInformation (μ.map Prod.swap) =
      measureMutualInformation μ

Uses 1

Statement usesMutual information of a joint probability measure

TheoremData-processing inequality#✓fully proved

If Z is produced from Y by a channel κ that does not see X (a Markov chain X → Y → Z), then I(X; Z) ≤ I(X; Y). The joint law of (X, Z) is (Kernel.id ∥ₖ κ) ∘ₘ μ.

theorem measureMutualInformation_comp_le (μ : ProbabilityMeasure (X × Y)) (κ : Kernel Y Z)
    [IsMarkovKernel κ] :
    measureMutualInformation
        (⟨(Kernel.id ∥ₖ κ) ∘ₘ (μ : Measure (X × Y)), inferInstance⟩ :
          ProbabilityMeasure (X × Z)) ≤
      measureMutualInformation μ

Uses 1 · Used by 1

Statement usesMutual information of a joint probability measure

Used byProcessing cannot increase information

TheoremProcessing cannot increase information#✓fully proved

I(X; g(Y)) ≤ I(X; Y) for a measurable g.

theorem measureMutualInformation_map_le (μ : ProbabilityMeasure (X × Y)) {g : Y → Z}
    (hg : Measurable g) :
    measureMutualInformation (μ.map (Prod.map id g)) ≤
      measureMutualInformation μ

Uses 2

Statement usesMutual information of a joint probability measure

Proof usesData-processing inequality

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.