E_gamma / hockey-stick divergence

Main definitions

• deGrootInfo

Main statements

• deGrootInfo_comp_le

Notation

Implementation details

noncomputable def ProbabilityTheory.eGamma {𝒳 : Type u_1} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (γ : ENNReal) : ENNReal

The hockey-stick divergence.

Equations

• ProbabilityTheory.eGamma μ ν γ = ProbabilityTheory.statInfo μ ν (MeasureTheory.Measure.dirac false + γ • MeasureTheory.Measure.dirac true)

theorem ProbabilityTheory.eGamma_comp_le {𝒳 : Type u_1} {𝒳' : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {m𝒳' : MeasurableSpace 𝒳'} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (γ : ENNReal) (η : ProbabilityTheory.Kernel 𝒳 𝒳') [ProbabilityTheory.IsMarkovKernel η] : ProbabilityTheory.eGamma (μ.bind ⇑η) (ν.bind ⇑η) γ ≤ ProbabilityTheory.eGamma μ ν γ

Data processing inequality for the hockey-stick divergence.