InformationTheory.Shannon.Bridge

Imports 10

Bridge: mutual information (KL form) ↔ conditional entropy #

For a finite alphabet X and a probability measure μ, (mutualInfo μ Xs Yo).toReal = entropy μ Xs - condEntropy μ Xs Yo.

Main statements #

mutualInfo_eq_entropy_sub_condEntropy — the bridge identity.

Implementation notes #

The proof establishes (μ.map (Xs, Yo)) ≪ (μ.map Xs).prod (μ.map Yo) on a finite alphabet, translates the KL divergence to a Bochner integral via toReal_klDiv_of_measure_eq, decomposes over the finite alphabet, and separates into H(X) - H(X|Y) by linearity.

noncomputable def

InformationTheory.Shannon.entropy

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} [Fintype X] [MeasurableSpace X] (μ : MeasureTheory.Measure Ω) (Xs : Ω → X) :

ℝ

Shannon entropy of a discrete random variable taking values in a finite alphabet.

Equations

InformationTheory.Shannon.entropy μ Xs = ∑ x : X, ((MeasureTheory.Measure.map Xs μ).real {x}).negMulLog

Instances For

Used by

theorem

InformationTheory.Shannon.entropy_nonneg

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} [Fintype X] [MeasurableSpace X] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : Ω → X) (hXs : Measurable Xs) :

0 ≤ entropy μ Xs

Used by

theorem

InformationTheory.Shannon.entropy_map_comp

source

{Ω : Type u_1} [MeasurableSpace Ω] {X : Type u_2} [Fintype X] [MeasurableSpace X] {Ω' : Type u_4} [MeasurableSpace Ω'] (μ : MeasureTheory.Measure Ω) {f : Ω → Ω'} (hf : Measurable f) {Xs : Ω' → X} (hXs : Measurable Xs) :

entropy (MeasureTheory.Measure.map f μ) Xs = entropy μ fun (ω : Ω) => Xs (f ω)

Used by

Helper lemmas for the bridge #

The bridge proof goes via three independent helpers:

klDiv_compProd_const_eq_lintegral: fiberwise expansion of conditional KL, klDiv (μ ⊗ₘ κ) (μ ⊗ₘ Kernel.const _ ν) = ∫⁻ x, klDiv (κ x) ν ∂μ. The Mathlib chain rule (klDiv_compProd_eq_add) only gives the non-fiberwise form; we need the integral identity to land at condEntropy.
klDiv_discrete_toReal_eq_sum: discrete klDiv on a finite alphabet expands as ∑ x, Q.real{x} * (log Q.real{x} - log P.real{x}).
integral_condDistrib_real_singleton_eq: marginal recovery, ∫ y, (condDistrib Xs Yo μ y).real {x} d(μ.map Yo) = (μ.map Xs).real {x}.

theorem

InformationTheory.Shannon.mutualInfo_eq_entropy_sub_condEntropy

source

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

(mutualInfo μ Xs Yo).toReal = entropy μ Xs - MeasureFano.condEntropy μ Xs Yo

For a finite-alphabet source X, (mutualInfo μ Xs Yo).toReal = entropy μ Xs - condEntropy μ Xs Yo.

Used by