Entropy of a measure

The Shannon entropy of a measure, following the PFR project's ForMathlib entropy, is Hm[μ] = ∑' s, negMulLog (((μ univ)⁻¹ • μ).real {s}), normalized so that a finite measure has the entropy of its probability normalization. On a finite type it falls short of log (card S) by the divergence from the uniform measure, so only that measure attains the bound. The mutual information of a measure on a product is Im[μ] = Hm[μ.fst] + Hm[μ.snd] - Hm[μ], on a finite type the divergence of the joint from its marginals' product, which a kernel on the second coordinate cannot increase.

Implementation notes

[UPSTREAM] candidate: mathlib has no Shannon entropy of a measure and no mutual information.

References

• [CT06], chapter 2.
• The PFR project, PFR/ForMathlib/Entropy/Measure.lean.

noncomputable def InformationTheory.measureEntropy {S : Type u_1} [MeasurableSpace S] (μ : MeasureTheory.Measure S) : ℝ

Entropy of a measure. The measure is normalized by (μ Set.univ)⁻¹, so that a finite measure has the entropy of its probability normalization and every other measure has entropy 0; on a probability measure simp removes the normalization.

Equations

• InformationTheory.measureEntropy μ = ∑' (s : S), (((μ Set.univ)⁻¹ • μ).real {s}).negMulLog

def InformationTheory.«termHm[_]» : Lean.ParserDescr

Entropy of a measure. The measure is normalized by (μ Set.univ)⁻¹, so that a finite measure has the entropy of its probability normalization and every other measure has entropy 0; on a probability measure simp removes the normalization.

Equations

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

@[simp]

theorem InformationTheory.measureEntropy_zero {S : Type u_1} [MeasurableSpace S] : measureEntropy 0 = 0

theorem InformationTheory.measureEntropy_of_not_isFiniteMeasure {S : Type u_1} [MeasurableSpace S] {μ : MeasureTheory.Measure S} (h : ¬MeasureTheory.IsFiniteMeasure μ) : measureEntropy μ = 0

theorem InformationTheory.measureEntropy_eq_tsum {S : Type u_1} [MeasurableSpace S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : measureEntropy μ = ∑' (s : S), (μ.real {s}).negMulLog

theorem InformationTheory.measureEntropy_eq_sum {S : Type u_1} [MeasurableSpace S] [Fintype S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : measureEntropy μ = ∑ s : S, (μ.real {s}).negMulLog

theorem InformationTheory.measureEntropy_eq_sum_finset {S : Type u_1} [MeasurableSpace S] {μ : MeasureTheory.Measure S} {A : Finset S} (hA : μ (↑A)ᶜ = 0) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : measureEntropy μ = ∑ s ∈ A, (μ.real {s}).negMulLog

The entropy of a probability measure carried by a finite set is a sum over that set.

theorem InformationTheory.measureEntropy_univ_smul {S : Type u_1} [MeasurableSpace S] {μ : MeasureTheory.Measure S} : measureEntropy ((μ Set.univ)⁻¹ • μ) = measureEntropy μ

theorem InformationTheory.measureEntropy_nonneg {S : Type u_1} [MeasurableSpace S] (μ : MeasureTheory.Measure S) : 0 ≤ measureEntropy μ

theorem InformationTheory.measureEntropy_map_of_injective {S : Type u_1} [MeasurableSpace S] {μ : MeasureTheory.Measure S} {U : Type u_3} [MeasurableSpace U] [MeasurableSingletonClass U] {f : S → U} (hf : Measurable f) (hinj : Function.Injective f) : measureEntropy (MeasureTheory.Measure.map f μ) = measureEntropy μ

Entropy is invariant under an injective recoding of the outcomes.

@[simp]

theorem InformationTheory.measureEntropy_dirac {S : Type u_1} [MeasurableSpace S] [MeasurableSingletonClass S] (x : S) : measureEntropy (MeasureTheory.Measure.dirac x) = 0

theorem InformationTheory.measureEntropy_uniformOn {S : Type u_1} [MeasurableSpace S] [MeasurableSingletonClass S] {A : Finset S} (hA : A.Nonempty) : measureEntropy (ProbabilityTheory.uniformOn ↑A) = Real.log ↑A.card

The entropy of the uniform measure on a finite set is the logarithm of its cardinality.

theorem InformationTheory.measureEntropy_eq_zero_iff {S : Type u_1} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] : measureEntropy μ = 0 ↔ ∃ (x : S), μ = MeasureTheory.Measure.dirac x

A probability measure on a finite type has zero entropy iff it is a Dirac mass.

theorem InformationTheory.toReal_klDiv_add_measureEntropy {S : Type u_1} [MeasurableSpace S] {μ : MeasureTheory.Measure S} [MeasurableSingletonClass S] [Fintype S] {ν : MeasureTheory.Measure S} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμν : μ.AbsolutelyContinuous ν) : (klDiv μ ν).toReal + measureEntropy μ = -∑ s : S, μ.real {s} * Real.log (ν.real {s})

The divergence and the entropy add up to the cross-entropy, the expected surprisal under μ of the atoms as ν weighs them.

theorem InformationTheory.toReal_klDiv_uniformOn_add_measureEntropy {S : Type u_1} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] [Nonempty S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] : (klDiv μ (ProbabilityTheory.uniformOn Set.univ)).toReal + measureEntropy μ = Real.log ↑(Fintype.card S)

The entropy of a probability measure on a finite type falls short of the logarithm of the cardinality by the divergence from the uniform measure.

theorem InformationTheory.measureEntropy_le_log_card {S : Type u_1} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] (μ : MeasureTheory.Measure S) : measureEntropy μ ≤ Real.log ↑(Fintype.card S)

Entropy is at most the logarithm of the cardinality of the type.

theorem InformationTheory.measureEntropy_eq_log_card_iff {S : Type u_1} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] [Nonempty S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] : measureEntropy μ = Real.log ↑(Fintype.card S) ↔ μ = ProbabilityTheory.uniformOn Set.univ

A probability measure on a finite type has entropy log (card S) only if it is uniform.

noncomputable def InformationTheory.measureMutualInfo {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] (μ : MeasureTheory.Measure (S × T)) : ℝ

The mutual information of a measure on a product is the sum of the entropies of its marginals less the entropy of the joint.

Equations

• InformationTheory.measureMutualInfo μ = InformationTheory.measureEntropy μ.fst + InformationTheory.measureEntropy μ.snd - InformationTheory.measureEntropy μ

def InformationTheory.«termIm[_]» : Lean.ParserDescr

The mutual information of a measure on a product is the sum of the entropies of its marginals less the entropy of the joint.

Equations

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

theorem InformationTheory.measureMutualInfo_map_swap {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (ρ : MeasureTheory.Measure (S × T)) : measureMutualInfo (MeasureTheory.Measure.map Prod.swap ρ) = measureMutualInfo ρ

Mutual information is symmetric in the two coordinates.

theorem InformationTheory.measureMutualInfo_eq_toReal_klDiv {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] [Fintype S] [Fintype T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure (S × T)) [MeasureTheory.IsProbabilityMeasure μ] : measureMutualInfo μ = (klDiv μ (μ.fst.prod μ.snd)).toReal

On a finite product, mutual information is the real part of the Kullback–Leibler divergence of the joint from the product of its marginals.

theorem InformationTheory.measureMutualInfo_nonneg {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] [Fintype S] [Fintype T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure (S × T)) [MeasureTheory.IsProbabilityMeasure μ] : 0 ≤ measureMutualInfo μ

theorem InformationTheory.measureMutualInfo_prod {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] [Fintype S] [Fintype T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (ν₁ : MeasureTheory.Measure S) (ν₂ : MeasureTheory.Measure T) [MeasureTheory.IsProbabilityMeasure ν₁] [MeasureTheory.IsProbabilityMeasure ν₂] : measureMutualInfo (ν₁.prod ν₂) = 0

A product measure carries no mutual information.

theorem InformationTheory.measureMutualInfo_parallelComp_id_comp_le {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] [Fintype S] [Fintype T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure (S × T)) [MeasureTheory.IsProbabilityMeasure μ] {U : Type u_3} [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (η : ProbabilityTheory.Kernel T U) [ProbabilityTheory.IsMarkovKernel η] : measureMutualInfo (μ.bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η)) ≤ measureMutualInfo μ

Data processing. Pushing the second coordinate through a Markov kernel cannot increase mutual information.