Entropy of a measure

The Shannon entropy of a measure on a measurable space, following the PFR project's ForMathlib entropy: Hm[μ] = ∑' s, negMulLog (((μ univ)⁻¹ • μ).real {s}), normalized so that a finite measure has the entropy of its probability normalization. Mutual information is the entropy difference Im[μ] = Hm[μ.fst] + Hm[μ.snd] - Hm[μ]; on a finite type it is the real part of the Kullback–Leibler divergence of the joint from the product of its marginals, hence nonnegative.

Random variables carry the same quantities through their laws: H[X ; μ] = Hm[μ.map X], the conditional entropy H[X | Y ; μ] as the expected entropy of X under Y = y, and I[X : Y ; μ]; on finite types the chain rule H[X, Y] = H[Y] + H[X | Y] holds and conditioning reduces entropy.

Main definitions

• measureEntropy, notation Hm[μ]; measureMutualInfo, notation Im[μ]
• entropy, notation H[X ; μ]; condEntropy, notation H[X | Y ; μ]; mutualInfo, notation I[X : Y ; μ]

Main results

• measureEntropy_le_log_card: entropy is at most the log of the cardinality; measureEntropy_uniformOn: the uniform measure attains it.
• measureMutualInfo_eq_toReal_klDiv, measureMutualInfo_nonneg, measureMutualInfo_parallelComp_id_comp_le (data processing).
• chain_rule, mutualInfo_eq_entropy_sub_condEntropy, condEntropy_le_entropy.
• condEntropy_uniformOn_univ: on a finite population under the uniform measure, conditional entropy is a formula in counts.

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_of_isProbabilityMeasure {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_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 μ

@[simp]

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

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_uniformOn {S : Type u_1} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] [DecidableEq 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.

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

Mutual information of a measure on a product: the entropies of the marginals less the entropy of the joint.

Equations

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

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

Mutual information of a measure on a product: the entropies of the marginals less the entropy of the joint.

Equations

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

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_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.

noncomputable def InformationTheory.entropy {S : Type u_1} [MeasurableSpace S] {Ω : Type u_3} [MeasurableSpace Ω] (X : Ω → S) (μ : MeasureTheory.Measure Ω) : ℝ

Entropy of a random variable: the entropy of its law.

Equations

• InformationTheory.entropy X μ = InformationTheory.measureEntropy (MeasureTheory.Measure.map X μ)

def InformationTheory.«termH[_;_]» : Lean.ParserDescr

Entropy of a random variable: the entropy of its law.

Equations

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

theorem InformationTheory.entropy_def {S : Type u_1} [MeasurableSpace S] {Ω : Type u_3} [MeasurableSpace Ω] (X : Ω → S) (μ : MeasureTheory.Measure Ω) : entropy X μ = measureEntropy (MeasureTheory.Measure.map X μ)

theorem InformationTheory.entropy_nonneg {S : Type u_1} [MeasurableSpace S] {Ω : Type u_3} [MeasurableSpace Ω] (X : Ω → S) (μ : MeasureTheory.Measure Ω) : 0 ≤ entropy X μ

@[simp]

theorem InformationTheory.entropy_zero_measure {S : Type u_1} [MeasurableSpace S] {Ω : Type u_3} [MeasurableSpace Ω] (X : Ω → S) : entropy X 0 = 0

theorem InformationTheory.entropy_le_log_card {S : Type u_1} [MeasurableSpace S] {Ω : Type u_3} [MeasurableSpace Ω] [Fintype S] [MeasurableSingletonClass S] (X : Ω → S) (μ : MeasureTheory.Measure Ω) : entropy X μ ≤ Real.log ↑(Fintype.card S)

theorem InformationTheory.entropy_eq_sum {S : Type u_1} [MeasurableSpace S] {Ω : Type u_3} [MeasurableSpace Ω] {X : Ω → S} [Fintype S] [MeasurableSingletonClass S] (hX : Measurable X) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : entropy X μ = ∑ s : S, (μ.real (X ⁻¹' {s})).negMulLog

noncomputable def InformationTheory.condEntropy {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) : ℝ

Conditional entropy: the expectation, under the law of Y, of the entropy of X conditioned on Y = y.

Equations

• InformationTheory.condEntropy X Y μ = ∫ (y : T), InformationTheory.entropy X μ[|Y ⁻¹' {y}] ∂MeasureTheory.Measure.map Y μ

def InformationTheory.«termH[_|_;_]» : Lean.ParserDescr

Conditional entropy: the expectation, under the law of Y, of the entropy of X conditioned on Y = y.

Equations

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

theorem InformationTheory.condEntropy_nonneg {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) : 0 ≤ condEntropy X Y μ

theorem InformationTheory.condEntropy_eq_sum {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] {Y : Ω → T} [Fintype T] [MeasurableSingletonClass T] (X : Ω → S) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : condEntropy X Y μ = ∑ y : T, μ.real (Y ⁻¹' {y}) * entropy X μ[|Y ⁻¹' {y}]

noncomputable def InformationTheory.mutualInfo {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) : ℝ

Mutual information of two random variables.

Equations

• InformationTheory.mutualInfo X Y μ = InformationTheory.entropy X μ + InformationTheory.entropy Y μ - InformationTheory.entropy (fun (ω : Ω) => (X ω, Y ω)) μ

def InformationTheory.«termI[_:_;_]» : Lean.ParserDescr

Mutual information of two random variables.

Equations

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

theorem InformationTheory.mutualInfo_def {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] (X : Ω → S) (Y : Ω → T) (μ : MeasureTheory.Measure Ω) : mutualInfo X Y μ = entropy X μ + entropy Y μ - entropy (fun (ω : Ω) => (X ω, Y ω)) μ

theorem InformationTheory.mutualInfo_eq_measureMutualInfo {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] {X : Ω → S} {Y : Ω → T} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) : mutualInfo X Y μ = measureMutualInfo (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω)) μ)

The mutual information of two random variables is that of their joint law.

theorem InformationTheory.mutualInfo_nonneg {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] {X : Ω → S} {Y : Ω → T} [Fintype S] [Fintype T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : 0 ≤ mutualInfo X Y μ

theorem InformationTheory.chain_rule {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] {X : Ω → S} {Y : Ω → T} [Fintype S] [Fintype T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : entropy (fun (ω : Ω) => (X ω, Y ω)) μ = entropy Y μ + condEntropy X Y μ

Chain rule: H[X, Y] = H[Y] + H[X | Y].

theorem InformationTheory.mutualInfo_eq_entropy_sub_condEntropy {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] {X : Ω → S} {Y : Ω → T} [Fintype S] [Fintype T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : mutualInfo X Y μ = entropy X μ - condEntropy X Y μ

theorem InformationTheory.condEntropy_le_entropy {S : Type u_1} {T : Type u_2} [MeasurableSpace S] [MeasurableSpace T] {Ω : Type u_3} [MeasurableSpace Ω] {X : Ω → S} {Y : Ω → T} [Fintype S] [Fintype T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : condEntropy X Y μ ≤ entropy X μ

Conditioning reduces entropy: H[X | Y] ≤ H[X].

Empirical entropies of a finite population

Under the uniform measure on a finite type, entropies are counts.

theorem InformationTheory.uniformOn_univ_cond {Ω : Type u_3} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Finite Ω] (A : Set Ω) : (ProbabilityTheory.uniformOn Set.univ)[|A] = ProbabilityTheory.uniformOn A

Conditioning the uniform measure on a finite type by a set restricts it to the set.

theorem InformationTheory.condEntropy_uniformOn_univ {Ω : Type u_3} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [Fintype Ω] {S : Type u_4} {T : Type u_5} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] [DecidableEq S] [MeasurableSpace T] [MeasurableSingletonClass T] [Fintype T] [DecidableEq T] (X : Ω → S) (Y : Ω → T) : condEntropy X Y (ProbabilityTheory.uniformOn Set.univ) = ∑ y : T, ↑{x : Ω | Y x = y}.card / ↑(Fintype.card Ω) * ∑ x : S, (↑{ω : Ω | Y ω = y ∧ X ω = x}.card / ↑{x : Ω | Y x = y}.card).negMulLog

The conditional entropy of one attribute of a finite population given another, under the uniform measure: each fibre of Y weighted by its share of the population, with the entropy of the distribution of X on the fibre, all as counts.