Conditional entropy and mutual information

DefinitionConditional entropy of a finite observation given a sub-\(\sigma\)-algebra#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(m\) be a sub-\(\sigma\)-algebra of the \(\sigma\)-algebra of \(\Omega\), let \(n \in \mathbb{N}\), and let \(f : \Omega \to \{0, \dots, n-1\}\) be measurable. For each \(i < n\) let \(P_i = \mathbb{E}_\mu[\mathbf{1}_{\{f = i\}} \mid m]\) be the conditional probability of \(\{f = i\}\) given \(m\). The quantized conditional entropy of \(f\) given \(m\), in bits, is

\[H_\mu(f \mid m) = \int_\Omega \sum_{i < n} -P_i(\omega) \log_2 P_i(\omega) \, d\mu(\omega),\]

with the convention \(0 \log_2 0 = 0\).

noncomputable def quantizedConditionalEntropy {Ω : Type*} [mΩ : MeasurableSpace Ω]
    (μ : ProbabilityMeasure Ω) (m : {m : MeasurableSpace Ω // m ≤ mΩ}) {n : ℕ}
    (f : Ω → Fin n) (_hf : Measurable f) : ℝ :=
  ∫ ω, (∑ i, Real.negMulLog
    (MeasureTheory.condExp m.1 μ.toMeasure (fun z => if f z = i then (1 : ℝ) else 0) ω)) /
      Real.log 2 ∂μ.toMeasure

Used by 4

Used byConditional Shannon entropy given a sub-\(\sigma\)-algebra · Conditional entropy of a constant output vanishes · Constant quantized observations have zero conditional entropy · One-valued observations have zero conditional entropy

TheoremOne-valued observations have zero conditional entropy#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\) and let \(m\) be a sub-\(\sigma\)-algebra of the \(\sigma\)-algebra of \(\Omega\). The quantized conditional entropy given \(m\) of the observation that is constantly \(0\), with values in the one-element set \(\{0\}\), is \(0\).

@[simp] theorem quantizedConditionalEntropy_singleton {Ω : Type*}
    [mΩ : MeasurableSpace Ω] (μ : ProbabilityMeasure Ω)
    (m : {m : MeasurableSpace Ω // m ≤ mΩ}) :
    quantizedConditionalEntropy μ m (fun _ : Ω => (0 : Fin 1)) measurable_const = 0

Uses 1

Statement usesConditional entropy of a finite observation given a sub-\(\sigma\)-algebra

TheoremConstant quantized observations have zero conditional entropy#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(m\) be a sub-\(\sigma\)-algebra of the \(\sigma\)-algebra of \(\Omega\), and let \(c \in \{0, \dots, n-1\}\) for some \(n \in \mathbb{N}\). The quantized conditional entropy given \(m\) of the constant observation \(\omega \mapsto c\) is \(0\).

@[simp] theorem quantizedConditionalEntropy_const {Ω : Type*}
    [mΩ : MeasurableSpace Ω] (μ : ProbabilityMeasure Ω)
    (m : {m : MeasurableSpace Ω // m ≤ mΩ}) {n : ℕ} (c : Fin n) :
    quantizedConditionalEntropy μ m (fun _ : Ω => c) measurable_const = 0

Uses 1 · Used by 1

Statement usesConditional entropy of a finite observation given a sub-\(\sigma\)-algebra

Used byConditional entropy of a constant output vanishes

DefinitionConditional Shannon entropy given a sub-\(\sigma\)-algebra#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(m\) be a sub-\(\sigma\)-algebra of the \(\sigma\)-algebra of \(\Omega\), and let \(X : \Omega \to Y\) be a measurable map into a measurable space \(Y\). The conditional Shannon entropy of \(X\) given \(m\) is the supremum in \([0, \infty]\), over all \(n \in \mathbb{N}\) and all measurable maps \(q : Y \to \{0, \dots, n-1\}\), of the quantized conditional entropy of \(q \circ X\) given \(m\), a negative value of the latter being counted as \(0\).

noncomputable def conditionalShannonEntropy {Ω Y : Type*}
    [mΩ : MeasurableSpace Ω] [MeasurableSpace Y] (μ : ProbabilityMeasure Ω)
    (m : {m : MeasurableSpace Ω // m ≤ mΩ}) (output : Ω → Y)
    (houtput : Measurable output) : ℝ≥0∞ :=
  sSup {h | ∃ (n : ℕ) (q : Y → Fin n) (hq : Measurable q),
    h = ENNReal.ofReal (quantizedConditionalEntropy μ m (q ∘ output) (hq.comp houtput))}

Sources

• the supremum over all finite measurable output quantizations.

Uses 1 · Used by 3

Statement usesConditional entropy of a finite observation given a sub-\(\sigma\)-algebra

Used byConditional entropy of the output given the auxiliary variable · Conditional entropy of the output given input and auxiliary variable · Conditional entropy of a constant output vanishes

TheoremConditional entropy of a constant output vanishes#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(m\) be a sub-\(\sigma\)-algebra of the \(\sigma\)-algebra of \(\Omega\), and let \(y\) be a point of a measurable space \(Y\). The conditional Shannon entropy given \(m\) of the constant output \(\omega \mapsto y\) is \(0\).

@[simp] theorem conditionalShannonEntropy_const {Ω Y : Type*}
    [mΩ : MeasurableSpace Ω] [MeasurableSpace Y] (μ : ProbabilityMeasure Ω)
    (m : {m : MeasurableSpace Ω // m ≤ mΩ}) (y : Y) :
    conditionalShannonEntropy μ m (fun _ : Ω => y) measurable_const = 0

Uses 3

Statement usesConditional Shannon entropy given a sub-\(\sigma\)-algebra

Proof usesConditional entropy of a finite observation given a sub-\(\sigma\)-algebra · Constant quantized observations have zero conditional entropy

DefinitionMutual information of a joint probability measure#✓fully proved

Let \(\mu\) be a probability measure on the product \(X \times Y\) of two measurable spaces, with marginals \(\mu_X\) and \(\mu_Y\). The mutual information of \(\mu\), in bits and possibly infinite, is

\[I(\mu) = \frac{D_{\mathrm{KL}}(\mu \parallel \mu_X \otimes \mu_Y)}{\ln 2} \in [0, \infty],\]

where \(D_{\mathrm{KL}}\) is the Kullback–Leibler divergence in nats.

noncomputable def measureMutualInformation {X Y : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] (μ : ProbabilityMeasure (X × Y)) : ℝ≥0∞ :=
  klDiv (μ : Measure (X × Y))
    (((μ : Measure (X × Y)).map Prod.fst).prod ((μ : Measure (X × Y)).map Prod.snd)) /
      ENNReal.ofReal (Real.log 2)

Sources

• KL divergence from the actual product of the actual marginals.

Used by 12

Used byZero information gain means independence · Information gain is mutual information · A functional representation has a measurable recovery map · Functional representation of a joint law · A functional representation has the prescribed joint law · Mutual information of a finite joint law · Mutual information vanishes exactly under independence · Mutual information of a finite joint law · Mutual information in terms of entropies · Data-processing inequality · Processing cannot increase information · Symmetry of mutual information

TheoremDivergence of a finite joint law from the product of its marginals#✓fully proved

Let \(\alpha\) and \(\beta\) be finite sets with measurable structures in which singletons are measurable, let \(p\) be a probability law on \(\alpha \times \beta\) with marginals \(p_X\) and \(p_Y\), and write \(H\) for Shannon entropy in bits. Then the Kullback–Leibler divergence of \(p\) from the product measure \(p_X \otimes p_Y\), computed with the natural logarithm and taken as a real number, equals \((H(p_X) + H(p_Y) - H(p)) \log 2\).

theorem toReal_klDiv_prod [Fintype α] [Fintype β] (p : PMF (α × β)) :
    (klDiv p.toMeasure ((p.map Prod.fst).toMeasure.prod (p.map Prod.snd).toMeasure)).toReal =
      (shannonEntropy (p.map Prod.fst) + shannonEntropy (p.map Prod.snd) - shannonEntropy p) *
        log 2

Uses 2 · Used by 2

Statement usesShannon entropy

Proof usesKullback–Leibler divergence on a finite space

Used byMutual information of a finite joint law · Subadditivity of entropy

TheoremSubadditivity of entropy#✓fully proved

Let \(p\) be a probability law on \(\alpha \times \beta\), where \(\alpha\) and \(\beta\) are finite, with marginals \(p_X\) and \(p_Y\). Writing \(H\) for Shannon entropy in bits, \(H(p) \le H(p_X) + H(p_Y)\).

theorem shannonEntropy_le_add [Fintype α] [Fintype β] (p : PMF (α × β)) :
    shannonEntropy p ≤ shannonEntropy (p.map Prod.fst) + shannonEntropy (p.map Prod.snd)

Uses 2 · Used by 2

Statement usesShannon entropy

Proof usesDivergence of a finite joint law from the product of its marginals

Used byConditioning does not increase entropy · Mutual information in terms of entropies

TheoremMutual information of a finite joint law#✓fully proved

Let \(p\) be a probability distribution on \(\alpha \times \beta\), where \(\alpha\) and \(\beta\) are finite measurable spaces in which every singleton is measurable, viewed as the joint law of a pair \((X, Y)\). Write \(H(X, Y)\), \(H(X)\) and \(H(Y)\) for the Shannon entropies of \(p\) and of its first and second marginals. Then the mutual information of the probability measure defined by \(p\), in bits, is the real number \(H(X) + H(Y) - H(X, Y)\) read as an element of \([0, \infty]\), a negative value being read as \(0\).

theorem measureMutualInformation_toMeasure [Fintype α] [Fintype β] (p : PMF (α × β)) :
    measureMutualInformation (⟨p.toMeasure, inferInstance⟩ : ProbabilityMeasure (α × β)) =
      ENNReal.ofReal
        (shannonEntropy (p.map Prod.fst) + shannonEntropy (p.map Prod.snd) - shannonEntropy p)

Uses 3 · Used by 2

Statement usesMutual information of a joint probability measure · Shannon entropy

Proof usesDivergence of a finite joint law from the product of its marginals

Used byInformation gain is mutual information · Mutual information in terms of entropies

TheoremMutual information vanishes exactly under independence#✓fully proved

Let \(p\) be a discrete probability distribution on \(\alpha \times \beta\), where \(\alpha\) and \(\beta\) are measurable spaces. The mutual information of the probability measure defined by \(p\) is \(0\) if and only if this measure equals the product of the probability measures defined by the two marginals of \(p\).

theorem measureMutualInformation_toMeasure_eq_zero_iff (p : PMF (α × β)) :
    measureMutualInformation (⟨p.toMeasure, inferInstance⟩ : ProbabilityMeasure (α × β)) = 0 ↔
      p.toMeasure = (p.map Prod.fst).toMeasure.prod (p.map Prod.snd).toMeasure

Uses 1 · Used by 1

Statement usesMutual information of a joint probability measure

Used byZero information gain means independence

DefinitionConditional entropy of a finite joint law#✓fully proved

Let \(p\) be a probability distribution on \(\alpha \times \beta\), where \(\alpha\) and \(\beta\) are finite, viewed as the joint law of a pair \((X, Y)\), and let \(p_X(a) = \sum_{b \in \beta} p(a, b)\) be its first marginal. The conditional entropy of \(Y\) given \(X\), in bits, is

\[H(Y \mid X) = -\sum_{a \in \alpha} \sum_{b \in \beta} p(a, b) \log_2 \frac{p(a, b)}{p_X(a)},\]

where every term with \(p(a, b) = 0\) is \(0\).

It is the finite counterpart of the conditional Shannon entropy given a sub-\(\sigma\)-algebra.

noncomputable def finiteConditionalEntropy [Fintype α] [Fintype β] (p : PMF (α × β)) : ℝ :=
  -∑ a, ∑ b, (p (a, b)).toReal * logb 2 ((p (a, b)).toReal / ((p.map Prod.fst) a).toReal)

Used by 5

Used byInformation gain of a split · Information gain in terms of entropies · No split has negative information gain · Conditioning does not increase entropy · Chain rule for entropy

TheoremChain rule for entropy#✓fully proved

Let \(p\) be a probability law on \(\alpha \times \beta\), where \(\alpha\) and \(\beta\) are finite, and let \(p_X\) be its first marginal. Write \(H(X, Y)\) for the Shannon entropy of \(p\), \(H(X)\) for the Shannon entropy of \(p_X\), and \(H(Y \mid X) = -\sum_{a, b} p(a, b) \log_2 (p(a, b) / p_X(a))\) for the finite conditional entropy of \(p\), all in bits. Then \(H(X, Y) = H(X) + H(Y \mid X)\).

theorem shannonEntropy_eq_add_finiteConditionalEntropy [Fintype α] [Fintype β]
    (p : PMF (α × β)) :
    shannonEntropy p = shannonEntropy (p.map Prod.fst) + finiteConditionalEntropy p

Uses 2 · Used by 2

Statement usesConditional entropy of a finite joint law · Shannon entropy

Used byInformation gain in terms of entropies · Conditioning does not increase entropy

TheoremConditioning does not increase entropy#✓fully proved

Let \(p\) be a probability distribution on \(\alpha \times \beta\), where \(\alpha\) and \(\beta\) are finite, viewed as the joint law of a pair \((X, Y)\). Then the conditional entropy \(H(Y \mid X)\) of \(p\) is at most the Shannon entropy \(H(Y)\) of the second marginal of \(p\), both in bits.

theorem finiteConditionalEntropy_le [Fintype α] [Fintype β] (p : PMF (α × β)) :
    finiteConditionalEntropy p ≤ shannonEntropy (p.map Prod.snd)

Uses 4 · Used by 1

Statement usesConditional entropy of a finite joint law · Shannon entropy

Proof usesChain rule for entropy · Subadditivity of entropy

Used byNo split has negative information gain

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.