Data processing inequality for f-divergences #
theorem
ProbabilityTheory.fDiv_comp_le_compProd_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
:
ProbabilityTheory.fDiv f (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd κ)
theorem
ProbabilityTheory.fDiv_comp_right_le''
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
:
ProbabilityTheory.fDiv f (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ ProbabilityTheory.fDiv f μ ν
The Data Processing Inequality for the f-divergence.
theorem
ProbabilityTheory.fDiv_comp_le_of_comp_le_of_ac
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure ν]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
(h : ∀ (μ : MeasureTheory.Measure α),
MeasureTheory.IsFiniteMeasure μ →
μ.AbsolutelyContinuous ν → ProbabilityTheory.fDiv f (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ ProbabilityTheory.fDiv f μ ν)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
:
ProbabilityTheory.fDiv f (μ.bind ⇑κ) (ν.bind ⇑κ) ≤ ProbabilityTheory.fDiv f μ ν
To prove the DPI for an f-divergence, it suffices to prove it under an absolute continuity hypothesis.