Conditional mutual information

TheoremSums against a pushforward of a finite law#✓fully proved

Summing a function of f t against p is summing against the pushforward p.map f.

theorem sum_toReal_mul_comp {τ δ : Type*} [Fintype τ] [Fintype δ] (p : PMF τ) (f : τ → δ)
    (φ : δ → ℝ) : ∑ t, (p t).toReal * φ (f t) = ∑ d, ((p.map f) d).toReal * φ d

Used by 1

Used byLog-sum against a pushforward equals its negative entropy

TheoremAtom mass is at most the mass of its image#✓fully proved

An atom's mass is at most the mass of its image.

theorem le_map_apply {τ δ : Type*} (p : PMF τ) (f : τ → δ) (t : τ) :
    p t ≤ (p.map f) (f t)

Used by 4

Used byChow–Liu approximation sums to one · Vanishing conditional mutual information iff conditional independence · Nonnegativity of conditional mutual information · Atom mass is at most the mass of its image, in reals

TheoremAtom mass is at most the mass of its image, in reals#✓fully proved

An atom's mass is at most the mass of its image, as real numbers.

theorem toReal_le_map_apply {τ δ : Type*} (p : PMF τ) (f : τ → δ) (t : τ) :
    (p t).toReal ≤ ((p.map f) (f t)).toReal

Uses 1 · Used by 3

Proof usesAtom mass is at most the mass of its image

Used byJoint law is absolutely continuous w.r.t. its Chow–Liu approximation · Chow–Liu identity · Conditional mutual information in terms of entropies

TheoremShannon entropy as a p log p sum#✓fully proved

Entropy times log 2 as a p log p sum.

theorem shannonEntropy_mul_log_two {δ : Type*} [Fintype δ] (q : PMF δ) :
    shannonEntropy q * log 2 = -∑ d, (q d).toReal * log (q d).toReal

Uses 1 · Used by 2

Statement usesShannon entropy

Used byChow–Liu identity · Log-sum against a pushforward equals its negative entropy

TheoremLog-sum against a pushforward equals its negative entropy#✓fully proved

∑ p(t) log (p.map f)(f t) = -H(p.map f) log 2.

theorem sum_mul_log_map {τ δ : Type*} [Fintype τ] [Fintype δ] (p : PMF τ) (f : τ → δ) :
    ∑ t, (p t).toReal * log ((p.map f) (f t)).toReal = -(shannonEntropy (p.map f) * log 2)

Uses 3 · Used by 2

Statement usesShannon entropy

Proof usesShannon entropy as a p log p sum · Sums against a pushforward of a finite law

Used byChow–Liu identity · Conditional mutual information in terms of entropies

TheoremEntropy of a pushforward is invariant under relabeling#✓fully proved

Relabeling the image of a map by a bijection preserves entropy.

theorem shannonEntropy_map_equiv_comp {τ δ ε : Type*} [Fintype δ] [Fintype ε] (p : PMF τ)
    (f : τ → δ) (e : δ ≃ ε) : shannonEntropy (p.map (e ∘ f)) = shannonEntropy (p.map f)

Uses 2 · Used by 2

Statement usesShannon entropy

Proof usesEntropy is invariant under relabeling

Used byData-processing inequality · Data-processing inequality

DefinitionMutual information of a finite joint law#✓fully proved

Mutual information I(X; Y) of a finite joint law p of (X, Y), in bits: the real value of measureMutualInformation on p, which is finite here (finiteMutualInformation_eq). Each finite alphabet carries the discrete σ-algebra.

noncomputable def finiteMutualInformation (p : PMF (α × β)) : ℝ :=
  letI : MeasurableSpace α := ⊤
  letI : MeasurableSpace β := ⊤
  (measureMutualInformation (⟨p.toMeasure, inferInstance⟩ : ProbabilityMeasure (α × β))).toReal

Uses 1 · Used by 6

Statement usesMutual information of a joint probability measure

Used byChow–Liu identity · Mutual-information weight of a dependence forest · Chain rule for mutual information · Mutual information in terms of entropies · Data-processing inequality · Data-processing inequality

TheoremMutual information in terms of entropies#✓fully proved

I(X; Y) = H(X) + H(Y) - H(X, Y) for a finite joint law.

theorem finiteMutualInformation_eq (p : PMF (α × β)) :
    finiteMutualInformation p =
      shannonEntropy (p.map Prod.fst) + shannonEntropy (p.map Prod.snd) - shannonEntropy p

Uses 5 · Used by 4

Statement usesMutual information of a finite joint law · Shannon entropy

Proof usesMutual information of a joint probability measure · Mutual information of a finite joint law · Subadditivity of entropy

Used byChow–Liu identity · Chain rule for mutual information · Data-processing inequality · Data-processing inequality

DefinitionConditional mutual information of a finite joint law#✓fully proved

The conditional mutual information I(X; Y | Z) of a finite joint law p of (X, Y, Z), in bits: ∑ p(x, y, z) log₂ (p(x, y, z) p(z) / (p(x, z) p(y, z))).

noncomputable def finiteConditionalMutualInformation (p : PMF (α × β × γ)) : ℝ :=
  ∑ a, ∑ b, ∑ c, (p (a, b, c)).toReal *
    logb 2 ((p (a, b, c)).toReal * ((p.map fun t ↦ t.2.2) c).toReal /
      (((p.map fun t ↦ (t.1, t.2.2)) (a, c)).toReal * ((p.map fun t ↦ t.2) (b, c)).toReal))

Used by 6

Used byConditional mutual information in terms of entropies · Vanishing conditional mutual information iff conditional independence · Nonnegativity of conditional mutual information · Chain rule for mutual information · Data-processing inequality · Data-processing inequality

TheoremConditional mutual information in terms of entropies#✓fully proved

I(X; Y | Z) = H(X, Z) + H(Y, Z) - H(X, Y, Z) - H(Z).

theorem finiteConditionalMutualInformation_eq (p : PMF (α × β × γ)) :
    finiteConditionalMutualInformation p =
      shannonEntropy (p.map fun t ↦ (t.1, t.2.2)) + shannonEntropy (p.map fun t ↦ t.2) -
        shannonEntropy p - shannonEntropy (p.map fun t ↦ t.2.2)

Uses 4 · Used by 3

Statement usesConditional mutual information of a finite joint law · Shannon entropy

Proof usesLog-sum against a pushforward equals its negative entropy · Atom mass is at most the mass of its image, in reals

Used byChain rule for mutual information · Data-processing inequality · Data-processing inequality

TheoremNonnegativity of conditional mutual information#✓fully proved

Conditional mutual information is nonnegative.

theorem finiteConditionalMutualInformation_nonneg (p : PMF (α × β × γ)) :
    0 ≤ finiteConditionalMutualInformation p

Uses 3 · Used by 2

Statement usesConditional mutual information of a finite joint law

Proof usesAtom mass is at most the mass of its image · Kullback–Leibler divergence of finite probability laws

Used byData-processing inequality · Data-processing inequality

TheoremVanishing conditional mutual information iff conditional independence#✓fully proved

I(X; Y | Z) = 0 exactly when X and Y are conditionally independent given Z: p(x, y, z) p(z) = p(x, z) p(y, z) for every atom.

theorem finiteConditionalMutualInformation_eq_zero_iff (p : PMF (α × β × γ)) :
    finiteConditionalMutualInformation p = 0 ↔
      ∀ a b c, p (a, b, c) * (p.map fun t ↦ t.2.2) c =
        (p.map fun t ↦ (t.1, t.2.2)) (a, c) * (p.map fun t ↦ t.2) (b, c)

Uses 3

Statement usesConditional mutual information of a finite joint law

Proof usesAtom mass is at most the mass of its image · Kullback–Leibler divergence of finite probability laws

TheoremChain rule for mutual information#✓fully proved

I(X; (Y, Z)) = I(X; Z) + I(X; Y | Z). Here p is read as a joint law of X and the pair (Y, Z).

theorem finiteMutualInformation_chain_rule (p : PMF (α × β × γ)) :
    finiteMutualInformation p =
      finiteMutualInformation (p.map fun t ↦ (t.1, t.2.2)) +
        finiteConditionalMutualInformation p

Uses 5

Statement usesConditional mutual information of a finite joint law · Mutual information of a finite joint law

Proof usesConditional mutual information in terms of entropies · Mutual information in terms of entropies · Shannon entropy

TheoremData-processing inequality#✓fully proved

Data-processing inequality, first half: if X and Z are conditionally independent given Y (a Markov chain X - Y - Z, stated as I(X; Z | Y) = 0 for the joint law p of (X, Y, Z)), then I(X; Z) ≤ I(X; Y).

theorem finiteMutualInformation_le_left_of_markov (p : PMF (α × β × γ))
    (hp : finiteConditionalMutualInformation (p.map fun t ↦ (t.1, t.2.2, t.2.1)) = 0) :
    finiteMutualInformation (p.map fun t ↦ (t.1, t.2.2)) ≤
      finiteMutualInformation (p.map fun t ↦ (t.1, t.2.1))

Uses 8

Statement usesConditional mutual information of a finite joint law · Mutual information of a finite joint law

Proof usesConditional mutual information in terms of entropies · Nonnegativity of conditional mutual information · Mutual information in terms of entropies · Shannon entropy · Entropy is invariant under relabeling · Entropy of a pushforward is invariant under relabeling

TheoremData-processing inequality#✓fully proved

Data-processing inequality, second half: under the same Markov condition, I(X; Z) ≤ I(Y; Z).

theorem finiteMutualInformation_le_right_of_markov (p : PMF (α × β × γ))
    (hp : finiteConditionalMutualInformation (p.map fun t ↦ (t.1, t.2.2, t.2.1)) = 0) :
    finiteMutualInformation (p.map fun t ↦ (t.1, t.2.2)) ≤
      finiteMutualInformation (p.map fun t ↦ t.2)

Uses 8

Statement usesConditional mutual information of a finite joint law · Mutual information of a finite joint law

Proof usesConditional mutual information in terms of entropies · Nonnegativity of conditional mutual information · Mutual information in terms of entropies · Shannon entropy · Entropy is invariant under relabeling · Entropy of a pushforward is invariant under relabeling

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.