DeGroot statistical information

Main definitions

• deGrootInfo

Main statements

• deGrootInfo_comp_le

Notation

Implementation details

noncomputable def ProbabilityTheory.deGrootInfo {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (p : ENNReal) (hp : p ≤ 1) : ENNReal

The DeGroot statistical information between two measures, for prior Bernoulli p.

Equations

• ProbabilityTheory.deGrootInfo μ ν p hp = ProbabilityTheory.statInfo μ ν (PMF.bernoulli p hp).toMeasure

theorem ProbabilityTheory.deGrootInfo_comp_le {𝒳 : Type u_1} {𝒳' : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {m𝒳' : MeasurableSpace 𝒳'} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (p : ENNReal) (hp : p ≤ 1) (η : ProbabilityTheory.Kernel 𝒳 𝒳') [ProbabilityTheory.IsMarkovKernel η] : ProbabilityTheory.deGrootInfo (μ.bind ⇑η) (ν.bind ⇑η) p hp ≤ ProbabilityTheory.deGrootInfo μ ν p hp

Data processing inequality for the DeGroot statistical information.