Skip to content

InformationTheory.Shannon.TypedRV

Imports 10

Typed random variable API #

An opt-in notation layer that allows writing H(μ; X), H(μ; X | Y), I(μ; X ; Y), I(μ; X ; Y | Z), and D(μ; X ∥ Y) directly in the style of Cover–Thomas.

Main definitions #

condEntropy — re-export of MeasureFano.condEntropy into the Shannon namespace.
klDivRV — KL divergence between two random variables: klDiv (μ.map X) (μ.map Y).
differentialEntropyRV — differential entropy of a real-valued random variable.

Main statements #

klDivRV_def — klDivRV μ X Y = klDiv (μ.map X) (μ.map Y) (by rfl).
entropy_nonneg_rv — 0 ≤ entropy μ X.
mutualInfo_comm_rv — I(X; Y) = I(Y; X).
mutualInfo_le_of_postprocess_rv — data processing inequality.

Implementation notes #

The internal representations (entropy, mutualInfo, condMutualInfo, MeasureFano.condEntropy, differentialEntropy, klDiv) are unchanged; only thin alias definitions and notation are added.

Notation is scoped[InformationTheory.Shannon] so that only call sites that open scoped InformationTheory.Shannon can see it.

The notation uses H(μ; X) / I(μ; X ; Y) forms with explicit μ because the _ anonymous-placeholder approach cannot synthesize μ from context at notation3 body evaluation time. Precedence :max makes each notation an atomic high-precedence term, avoiding parse errors in expressions like 0 ≤ H(μ; X).

The separator in D(μ; X ∥ Y) is ∥ (U+2225 PARALLEL TO), distinct from the norm delimiter ‖ (U+2016 DOUBLE VERTICAL LINE), to avoid token conflicts.

Type-class constraints required by each notation propagate to the call site:

H(μ; X) / H(μ; X | Y) require [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α].
I(μ; X ; Y) requires [MeasurableSpace α] [MeasurableSpace β].
I(μ; X ; Y | Z) additionally requires [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace β] [Nonempty β].
D(μ; X ∥ Y) requires [MeasurableSpace α].

Re-export: `MeasureFano.condEntropy` #

noncomputable def

InformationTheory.Shannon.condEntropy

@[reducible]

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (Xs : Ω → α) (Yo : Ω → β) :

Re-export InformationTheory.MeasureFano.condEntropy into the InformationTheory.Shannon namespace, so the notation H(X | Y) resolves here. Internal definition is unchanged.

Equations

InformationTheory.Shannon.condEntropy μ Xs Yo = InformationTheory.MeasureFano.condEntropy μ Xs Yo

Instances For

Used by

KL divergence (typed RV form, 1-measure) #

noncomputable def

InformationTheory.Shannon.klDivRV

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

KL divergence between two random variables on a common ambient measure μ: klDivRV μ X Y := klDiv (μ.map X) (μ.map Y).

This is the 1-measure form of the textbook D(X ‖ Y). The 2-measure form (klDiv (μ.map X) (ν.map Y)) is not provided here.

Equations

InformationTheory.Shannon.klDivRV μ X Y = InformationTheory.klDiv (MeasureTheory.Measure.map X μ) (MeasureTheory.Measure.map Y μ)

Instances For

Used by

theorem

InformationTheory.Shannon.klDivRV_def

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

klDivRV μ X Y = klDiv (MeasureTheory.Measure.map X μ) (MeasureTheory.Measure.map Y μ)

klDivRV μ X Y = klDiv (μ.map X) (μ.map Y) by definition.

Used by

Differential entropy (typed RV form) #

noncomputable def

InformationTheory.Shannon.differentialEntropyRV

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

Differential entropy of a real-valued random variable on ambient (Ω, μ): differentialEntropyRV μ X := differentialEntropy (μ.map X).

Equations

InformationTheory.Shannon.differentialEntropyRV μ X = InformationTheory.Shannon.differentialEntropy (MeasureTheory.Measure.map X μ)

Instances For

Used by

Notation #

def

InformationTheory.Shannon.«termH(_;_)»

:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

InformationTheory.Shannon.«termH(_;_|_)»

:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

InformationTheory.Shannon.«termI(_;_;_)»

:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

InformationTheory.Shannon.«termI(_;_;_|_)»

:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

InformationTheory.Shannon.«termD(_;_∥_)»

:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

Sanity examples #

Typed-form main lemmas #

One-line aliases of the measure-form lemmas. The _rv suffix avoids name conflicts with the bare names.

Entropy #

theorem

InformationTheory.Shannon.entropy_nonneg_rv

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → α) (hX : Measurable X) :

0 ≤ entropy μ X

H(X) ≥ 0.

Used by

Mutual information #

theorem

InformationTheory.Shannon.mutualInfo_comm_rv

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] {β : Type u_3} [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY : Measurable Y) :

mutualInfo μ X Y = mutualInfo μ Y X

I(X; Y) = I(Y; X) (Cover–Thomas).

Used by

Data processing inequality #

theorem

InformationTheory.Shannon.mutualInfo_le_of_postprocess_rv

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [MeasurableSpace α] {β : Type u_3} [MeasurableSpace β] {γ : Type u_4} [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY : Measurable Y) {f : β → γ} (hf : Measurable f) :

mutualInfo μ X (f ∘ Y) ≤ mutualInfo μ X Y

Data processing inequality: post-processing cannot increase mutual information. I(X; f(Y)) ≤ I(X; Y) — Cover–Thomas.

Used by

Sanity examples for typed-form main lemmas #