Entropy of a measure

Main definitions

• measureEntropy: entropy of a measure μ, denoted by Hm[μ]
• measureMutualInfo: mutual information of a measure over a product space, denoted by Im[μ], equal to Hm[μ.map Prod.fst] + Hm[μ.map Prod.snd] - Hm[μ]

Notations

• Hm[μ] = measureEntropy μ
• Im[μ] = measureMutualInfo μ

noncomputable def ProbabilityTheory.measureEntropy {S : Type u_2} [MeasurableSpace S] (μ : autoParam (MeasureTheory.Measure S) _auto✝) : ℝ

Entropy of a measure on a measurable space.

We normalize the measure by (μ Set.univ)⁻¹ to extend the entropy definition to finite measures. What we really want to do is deal with μ=0 or IsProbabilityMeasure μ, but we don't have a typeclass for that (we could create one though). The added complexity in the expression is not an issue because if μ is a probability measure, a call to simp will simplify (μ Set.univ)⁻¹ • μ to μ.

Equations

• Hm[μ] = ∑' (s : S), (((μ Set.univ)⁻¹ • μ) {s}).toReal.negMulLog

theorem ProbabilityTheory.measureEntropy_def {S : Type u_2} [MeasurableSpace S] (μ : MeasureTheory.Measure S) : Hm[μ] = ∑' (s : S), (((μ Set.univ)⁻¹ • μ) {s}).toReal.negMulLog

theorem ProbabilityTheory.measureEntropy_def' {S : Type u_2} [MeasurableSpace S] (μ : MeasureTheory.Measure S) : Hm[μ] = ∑' (s : S), (((μ.real Set.univ)⁻¹ • μ.real) {s}).negMulLog

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

Entropy of a measure on a measurable space.

We normalize the measure by (μ Set.univ)⁻¹ to extend the entropy definition to finite measures. What we really want to do is deal with μ=0 or IsProbabilityMeasure μ, but we don't have a typeclass for that (we could create one though). The added complexity in the expression is not an issue because if μ is a probability measure, a call to simp will simplify (μ Set.univ)⁻¹ • μ to μ.

Equations

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

class ProbabilityTheory.FiniteSupport {S : Type u_2} [MeasurableSpace S] (μ : autoParam (MeasureTheory.Measure S) _auto✝) : Prop

A measure has finite support if there exists a finite set whose complement has zero measure.

• finite : ∃ (A : Finset S), μ (↑A)ᶜ = 0

theorem ProbabilityTheory.FiniteSupport.finite {S : Type u_2} : ∀ {inst : MeasurableSpace S} {μ : autoParam (MeasureTheory.Measure S) _auto✝} [self : ProbabilityTheory.FiniteSupport μ], ∃ (A : Finset S), μ (↑A)ᶜ = 0

noncomputable def MeasureTheory.Measure.support {S : Type u_2} [MeasurableSpace S] (μ : MeasureTheory.Measure S) [hμ : ProbabilityTheory.FiniteSupport μ] : Finset S

A set on which a measure with finite support is supported.

Equations

• μ.support = Finset.filter (fun (x : S) => μ {x} ≠ 0) ⋯.choose

theorem ProbabilityTheory.measure_compl_support {S : Type u_2} [MeasurableSpace S] (μ : MeasureTheory.Measure S) [hμ : ProbabilityTheory.FiniteSupport μ] : μ (↑μ.support)ᶜ = 0

@[simp]

theorem ProbabilityTheory.mem_support {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} [hμ : ProbabilityTheory.FiniteSupport μ] {x : S} : x ∈ μ.support ↔ μ {x} ≠ 0

instance ProbabilityTheory.finiteSupport_zero {S : Type u_2} [MeasurableSpace S] : ProbabilityTheory.FiniteSupport 0

Equations

• ⋯ = ⋯

noncomputable def ProbabilityTheory.FiniteEntropy {S : Type u_2} [MeasurableSpace S] (μ : autoParam (MeasureTheory.Measure S) _auto✝) : Prop

TODO: replace FiniteSupport hypotheses in these files with FiniteEntropy hypotheses.

Equations

• ProbabilityTheory.FiniteEntropy μ = ((Summable fun (s : S) => (((μ Set.univ)⁻¹ • μ) {s}).toReal.negMulLog) ∧ ∃ (A : Set S), Countable ↑A ∧ μ Aᶜ = 0)

instance ProbabilityTheory.finiteSupport_of_fintype {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} [Fintype S] : ProbabilityTheory.FiniteSupport μ

Equations

• ⋯ = ⋯

instance ProbabilityTheory.finiteSupport_of_mul {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} [ProbabilityTheory.FiniteSupport μ] (c : ENNReal) : ProbabilityTheory.FiniteSupport (c • μ)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.finiteSupport_of_comp {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] {μ : MeasureTheory.Measure Ω} [ProbabilityTheory.FiniteSupport μ] {X : Ω → S} (hX : Measurable X) : ProbabilityTheory.FiniteSupport (MeasureTheory.Measure.map X μ)

instance ProbabilityTheory.finiteSupport_of_dirac {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] (x : S) : ProbabilityTheory.FiniteSupport (MeasureTheory.Measure.dirac x)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.full_measure_of_finiteRange {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] {μ : MeasureTheory.Measure Ω} {X : Ω → S} (hX : Measurable X) [hX' : FiniteRange X] : (MeasureTheory.Measure.map X μ) (↑(FiniteRange.toFinset X))ᶜ = 0

duplicate of FiniteRange.null_of_compl

instance ProbabilityTheory.finiteSupport_of_finiteRange {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSingletonClass S] {μ : MeasureTheory.Measure Ω} {X : Ω → S} [hX' : FiniteRange X] : ProbabilityTheory.FiniteSupport (MeasureTheory.Measure.map X μ)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.finiteSupport_of_prod {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] {μ : MeasureTheory.Measure S} [ProbabilityTheory.FiniteSupport μ] {ν : MeasureTheory.Measure T} [MeasureTheory.SigmaFinite ν] [ProbabilityTheory.FiniteSupport ν] : ProbabilityTheory.FiniteSupport (μ.prod ν)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.integrable_of_finiteSupport {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) [ProbabilityTheory.FiniteSupport μ] {β : Type u_5} [NormedAddCommGroup β] [MeasureTheory.IsFiniteMeasure μ] [Countable S] {f : S → β} : MeasureTheory.Integrable f μ

The countability hypothesis can probably be dropped here. Proof is unwieldy and can probably be golfed.

theorem ProbabilityTheory.integral_congr_finiteSupport {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {f : Ω → G} {g : Ω → G} [ProbabilityTheory.FiniteSupport μ] (hfg : ∀ (x : Ω), μ {x} ≠ 0 → f x = g x) : ∫ (x : Ω), f x ∂μ = ∫ (x : Ω), g x ∂μ

theorem ProbabilityTheory.Measure.ext_iff_singleton_finiteSupport {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] {μ1 : MeasureTheory.Measure S} {μ2 : MeasureTheory.Measure S} [ProbabilityTheory.FiniteSupport μ1] [ProbabilityTheory.FiniteSupport μ2] : μ1 = μ2 ↔ ∀ (x : S), μ1 {x} = μ2 {x}

This generalizes Measure.ext_iff_singleton in MeasureReal

theorem ProbabilityTheory.Measure.ext_iff_measureReal_singleton_finiteSupport {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] {μ1 : MeasureTheory.Measure S} {μ2 : MeasureTheory.Measure S} [ProbabilityTheory.FiniteSupport μ1] [ProbabilityTheory.FiniteSupport μ2] [MeasureTheory.IsFiniteMeasure μ1] [MeasureTheory.IsFiniteMeasure μ2] : μ1 = μ2 ↔ ∀ (x : S), μ1.real {x} = μ2.real {x}

theorem ProbabilityTheory.measureEntropy_def_finite {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} {A : Finset S} (hA : μ (↑A)ᶜ = 0) : Hm[μ] = ∑ s ∈ A, (((μ Set.univ)⁻¹ • μ) {s}).toReal.negMulLog

theorem ProbabilityTheory.measureEntropy_def_finite' {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} {A : Finset S} (hA : μ (↑A)ᶜ = 0) : Hm[μ] = ∑ s ∈ A, (((μ.real Set.univ)⁻¹ • μ.real) {s}).negMulLog

@[simp]

theorem ProbabilityTheory.measureEntropy_zero {S : Type u_2} [MeasurableSpace S] : Hm[0] = 0

@[simp]

theorem ProbabilityTheory.measureEntropy_dirac {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] (x : S) : Hm[MeasureTheory.Measure.dirac x] = 0

theorem ProbabilityTheory.measureEntropy_of_not_isFiniteMeasure {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} (h : ¬MeasureTheory.IsFiniteMeasure μ) : Hm[μ] = 0

theorem ProbabilityTheory.measureEntropy_of_isProbabilityMeasure {S : Type u_2} [MeasurableSpace S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : Hm[μ] = ∑' (s : S), (μ {s}).toReal.negMulLog

theorem ProbabilityTheory.measureEntropy_of_isProbabilityMeasure' {S : Type u_2} [MeasurableSpace S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : Hm[μ] = ∑' (s : S), (μ.real {s}).negMulLog

theorem ProbabilityTheory.measureEntropy_of_isProbabilityMeasure_finite {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} {A : Finset S} (hA : μ (↑A)ᶜ = 0) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : Hm[μ] = ∑ s ∈ A, (μ {s}).toReal.negMulLog

theorem ProbabilityTheory.measureEntropy_of_isProbabilityMeasure_finite' {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} {A : Finset S} (hA : μ (↑A)ᶜ = 0) [MeasureTheory.IsZeroOrProbabilityMeasure μ] : Hm[μ] = ∑ s ∈ A, (μ.real {s}).negMulLog

theorem ProbabilityTheory.measureEntropy_univ_smul {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} : Hm[(μ Set.univ)⁻¹ • μ] = Hm[μ]

theorem ProbabilityTheory.measureEntropy_nonneg {S : Type u_2} [MeasurableSpace S] (μ : MeasureTheory.Measure S) : 0 ≤ Hm[μ]

theorem ProbabilityTheory.measureEntropy_le_card_aux {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] {μ : MeasureTheory.Measure S} [MeasureTheory.IsProbabilityMeasure μ] (A : Finset S) (hμ : μ (↑A)ᶜ = 0) : Hm[μ] ≤ Real.log ↑A.card

Auxiliary lemma for measureEntropy_le_log_card_of_mem, which removes the probability measure assumption.

theorem ProbabilityTheory.measureEntropy_eq_card_iff_measureReal_eq_aux {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] : Hm[μ] = Real.log ↑(Fintype.card S) ↔ ∀ (s : S), μ.real {s} = (↑(Fintype.card S))⁻¹

theorem ProbabilityTheory.measureEntropy_eq_card_iff_measure_eq_aux {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) [Fintype S] [MeasureTheory.IsProbabilityMeasure μ] : Hm[μ] = Real.log ↑(Fintype.card S) ↔ ∀ (s : S), μ {s} = ↑(↑(Fintype.card S))⁻¹

theorem ProbabilityTheory.measureEntropy_le_log_card_of_mem {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] {A : Finset S} (μ : MeasureTheory.Measure S) (hμA : μ (↑A)ᶜ = 0) : Hm[μ] ≤ Real.log ↑(Nat.card { x : S // x ∈ A })

theorem ProbabilityTheory.measureEntropy_le_log_card {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] [Fintype S] (μ : MeasureTheory.Measure S) : Hm[μ] ≤ Real.log ↑(Fintype.card S)

theorem ProbabilityTheory.measureEntropy_eq_card_iff_measureReal_eq {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} [MeasurableSingletonClass S] [Fintype S] [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] : Hm[μ] = Real.log ↑(Fintype.card S) ↔ ∀ (s : S), μ.real {s} = μ.real Set.univ / ↑(Fintype.card S)

theorem ProbabilityTheory.measureEntropy_eq_card_iff_measure_eq {S : Type u_2} [MeasurableSpace S] {μ : MeasureTheory.Measure S} [MeasurableSingletonClass S] [Fintype S] [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] : Hm[μ] = Real.log ↑(Fintype.card S) ↔ ∀ (s : S), μ {s} = μ Set.univ / ↑(Fintype.card S)

theorem ProbabilityTheory.measureEntropy_map_of_injective {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] (μ : MeasureTheory.Measure T) (f : T → S) (hf_m : Measurable f) (hf : Function.Injective f) : Hm[MeasureTheory.Measure.map f μ] = Hm[μ]

theorem ProbabilityTheory.measureEntropy_comap {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] (μ : MeasureTheory.Measure T) (f : S → T) (hf : MeasurableEmbedding f) (hf_range : Set.range f =ᵐ[μ] Set.univ) : Hm[MeasureTheory.Measure.comap f μ] = Hm[μ]

theorem ProbabilityTheory.measureEntropy_comap_equiv {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] (μ : MeasureTheory.Measure T) (f : S ≃ᵐ T) : Hm[MeasureTheory.Measure.comap (⇑f) μ] = Hm[μ]

@[simp]

theorem ProbabilityTheory.measureEntropy_prod {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] {μ : MeasureTheory.Measure S} {ν : MeasureTheory.Measure T} [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [MeasurableSingletonClass T] : Hm[μ.prod ν] = Hm[μ] + Hm[ν]

An ambitious goal would be to replace FiniteSupport with finite entropy.

noncomputable def ProbabilityTheory.measureMutualInfo {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (μ : autoParam (MeasureTheory.Measure (S × T)) _auto✝) : ℝ

The mutual information between the marginals of a measure on a product space.

Equations

• Im[μ] = Hm[MeasureTheory.Measure.map Prod.fst μ] + Hm[MeasureTheory.Measure.map Prod.snd μ] - Hm[μ]

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

The mutual information between the marginals of a measure on a product space.

Equations

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

theorem ProbabilityTheory.measureMutualInfo_def {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (μ : MeasureTheory.Measure (S × T)) : Im[μ] = Hm[MeasureTheory.Measure.map Prod.fst μ] + Hm[MeasureTheory.Measure.map Prod.snd μ] - Hm[μ]

@[simp]

theorem ProbabilityTheory.measureMutualInfo_zero_measure {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] : Im[0] = 0

theorem ProbabilityTheory.measureMutualInfo_of_not_isFiniteMeasure {S : Type u_2} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace U] {μ : MeasureTheory.Measure (S × U)} (h : ¬MeasureTheory.IsFiniteMeasure μ) : Im[μ] = 0

theorem ProbabilityTheory.measureMutualInfo_univ_smul {S : Type u_2} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace U] (μ : MeasureTheory.Measure (S × U)) : Im[(μ Set.univ)⁻¹ • μ] = Im[μ]

theorem ProbabilityTheory.measureMutualInfo_swap {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure (S × T)) : Im[MeasureTheory.Measure.map Prod.swap μ] = Im[μ]

@[simp]

theorem ProbabilityTheory.measureMutualInfo_prod {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure S} {ν : MeasureTheory.Measure T} [ProbabilityTheory.FiniteSupport μ] [ProbabilityTheory.FiniteSupport ν] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : Im[μ.prod ν] = 0

theorem ProbabilityTheory.measureMutualInfo_nonneg_aux {S : Type u_2} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace U] [MeasurableSingletonClass S] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure (S × U)} [ProbabilityTheory.FiniteSupport μ] [MeasureTheory.IsZeroOrProbabilityMeasure μ] : 0 ≤ Im[μ] ∧ (Im[μ] = 0 ↔ ∀ (p : S × U), μ.real {p} = (MeasureTheory.Measure.map Prod.fst μ).real {p.1} * (MeasureTheory.Measure.map Prod.snd μ).real {p.2})

An ambitious goal would be to replace FiniteSupport with finite entropy. Proof is long and slow; needs to be optimized

theorem ProbabilityTheory.measureMutualInfo_nonneg {S : Type u_2} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace U] [MeasurableSingletonClass S] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure (S × U)} [ProbabilityTheory.FiniteSupport μ] : 0 ≤ Im[μ]

theorem ProbabilityTheory.measureMutualInfo_eq_zero_iff {S : Type u_2} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace U] [MeasurableSingletonClass S] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure (S × U)} [ProbabilityTheory.FiniteSupport μ] [MeasureTheory.IsZeroOrProbabilityMeasure μ] : Im[μ] = 0 ↔ ∀ (p : S × U), μ.real {p} = (MeasureTheory.Measure.map Prod.fst μ).real {p.1} * (MeasureTheory.Measure.map Prod.snd μ).real {p.2}