InformationTheory.Shannon.Entropy

Imports 4

Entropy chain rule and conditioning monotonicity #

Two-variable Shannon inequalities: chain rule, conditional mutual information formula, and the fact that conditioning never increases entropy.

Main statements #

entropy_pair_eq_entropy_add_condEntropy — H(X, Y) = H(X) + H(Y | X).
condEntropy_tower — disintegration form of H(X | Y, Z).
condMutualInfo_eq_condEntropy_sub_condEntropy — I(X; Z | Y) = H(X | Y) - H(X | Y, Z).
condEntropy_le_condEntropy_of_pair — H(X | Y, Z) ≤ H(X | Y).

Implementation notes #

condMutualInfo_eq_condEntropy_sub_condEntropy uses the Mathlib mutual-information chain rule mutualInfo_chain_rule plus mutualInfo_comm/condMutualInfo_comm to put Xs on the left, then lifts to .toReal using finiteness from mutualInfo_ne_top and condMutualInfo_ne_top.

theorem

InformationTheory.Shannon.entropy_pair_eq_entropy_add_condEntropy

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] {Y : Type u_3} [Fintype Y] [Nonempty Y] [MeasurableSpace Y] [MeasurableSingletonClass Y] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → X) (Yo : Ω → Y) (_hXs : Measurable Xs) (hYo : Measurable Yo) :

(entropy μ fun (ω : Ω) => (Xs ω, Yo ω)) = entropy μ Xs + MeasureFano.condEntropy μ Yo Xs

Chain rule for Shannon entropy: H(X, Y) = H(X) + H(Y | X).

Used by

theorem

InformationTheory.Shannon.condEntropy_tower

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} [Fintype X] [Nonempty X] [MeasurableSpace X] [MeasurableSingletonClass X] {Y : Type u_3} [MeasurableSpace Y] {Z : Type u_4} [Fintype Z] [Nonempty Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → X) (Yo : Ω → Y) (Zo : Ω → Z) (_hXs : Measurable Xs) (_hYo : Measurable Yo) (hZo : Measurable Zo) :

(MeasureFano.condEntropy μ Xs fun (ω : Ω) => (Yo ω, Zo ω)) = ∫ (y : Y), ∫ (z : Z), ∑ x : X, (((ProbabilityTheory.condDistrib Xs (fun (ω : Ω) => (Yo ω, Zo ω)) μ) (y, z)).real {x}).negMulLog ∂(ProbabilityTheory.condDistrib Zo Yo μ) y ∂MeasureTheory.Measure.map Yo μ

Tower of conditional entropy: disintegrating the joint conditioner (Y, Z) into Z given Y followed by Y, H(X | Y, Z) = ∫ y, ∫ z, Σ x, negMulLog (condDistrib X (Y,Z) μ (y,z) {x}) d(condDistrib Z Y μ y) d P_Y.

The inner expression Σ x, negMulLog (condDistrib X (Y,Z) μ (y,z) {x}) is the slice-wise Shannon entropy of X conditioned on the simultaneous value of Y and Z. The two outer integrals build back up to H(X | Y, Z). Required as a lemma for the middle result condMutualInfo_eq_condEntropy_sub_condEntropy.

Used by

theorem

InformationTheory.Shannon.condMutualInfo_eq_condEntropy_sub_condEntropy

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} [Fintype X] [Nonempty X] [MeasurableSpace X] [MeasurableSingletonClass X] {Y : Type u_3} [Fintype Y] [MeasurableSpace Y] [MeasurableSingletonClass Y] {Z : Type u_4} [Fintype Z] [Nonempty Z] [MeasurableSpace Z] [MeasurableSingletonClass Z] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → X) (Yo : Ω → Y) (Zo : Ω → Z) (hXs : Measurable Xs) (hYo : Measurable Yo) (hZo : Measurable Zo) :

(condMutualInfo μ Xs Zo Yo).toReal = MeasureFano.condEntropy μ Xs Yo - MeasureFano.condEntropy μ Xs fun (ω : Ω) => (Yo ω, Zo ω)

Conditional mutual information formula: I(X; Z | Y) = H(X | Y) - H(X | Y, Z).

Used by

theorem

InformationTheory.Shannon.condEntropy_le_condEntropy_of_pair

source

(MeasureFano.condEntropy μ Xs fun (ω : Ω) => (Yo ω, Zo ω)) ≤ MeasureFano.condEntropy μ Xs Yo

Conditioning never increases entropy: H(X | Y, Z) ≤ H(X | Y). Direct corollary of the middle lemma condMutualInfo_eq_condEntropy_sub_condEntropy and condMutualInfo_nonneg. The n-variable Han inequality reduces to iterating this on prefixes of Fin n.

Used by