fDiv and StatInfo #
theorem
ProbabilityTheory.fDiv_statInfoFun_comp_right_le
{𝒳 : Type u_1}
{𝒳' : Type u_2}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(η : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel η]
(hβ : 0 ≤ β)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) (μ.bind ⇑η) (ν.bind ⇑η) ≤ ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν
Data processing inequality for the f-divergence of statInfoFun.
theorem
ProbabilityTheory.fDiv_comp_right_le'
{𝒳 : Type u_1}
{𝒳' : Type u_2}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(η : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel η]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
ProbabilityTheory.fDiv f (μ.bind ⇑η) (ν.bind ⇑η) ≤ ProbabilityTheory.fDiv f μ ν
Data processing inequality for the f-divergence.
theorem
ProbabilityTheory.fDiv_fst_le'
{𝒳 : Type u_1}
{𝒳' : Type u_2}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{f : ℝ → ℝ}
(μ : MeasureTheory.Measure (𝒳 × 𝒳'))
(ν : MeasureTheory.Measure (𝒳 × 𝒳'))
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
ProbabilityTheory.fDiv f μ.fst ν.fst ≤ ProbabilityTheory.fDiv f μ ν
theorem
ProbabilityTheory.fDiv_snd_le'
{𝒳 : Type u_1}
{𝒳' : Type u_2}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{f : ℝ → ℝ}
(μ : MeasureTheory.Measure (𝒳 × 𝒳'))
(ν : MeasureTheory.Measure (𝒳 × 𝒳'))
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
ProbabilityTheory.fDiv f μ.snd ν.snd ≤ ProbabilityTheory.fDiv f μ ν
theorem
ProbabilityTheory.le_fDiv_compProd'
{𝒳 : Type u_1}
{𝒳' : Type u_2}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel 𝒳 𝒳')
(η : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
ProbabilityTheory.fDiv f μ ν ≤ ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd η)
theorem
ProbabilityTheory.fDiv_compProd_right'
{𝒳 : Type u_1}
{𝒳' : Type u_2}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel κ]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd κ) = ProbabilityTheory.fDiv f μ ν
theorem
ProbabilityTheory.fDiv_comp_le_compProd'
{𝒳 : Type u_1}
{𝒳' : Type u_2}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(κ : ProbabilityTheory.Kernel 𝒳 𝒳')
(η : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
ProbabilityTheory.fDiv f (μ.bind ⇑κ) (ν.bind ⇑η) ≤ ProbabilityTheory.fDiv f (μ.compProd κ) (ν.compProd η)
theorem
ProbabilityTheory.fDiv_comp_le_compProd_right'
{𝒳 : Type u_1}
{𝒳' : Type u_2}
{m𝒳 : MeasurableSpace 𝒳}
{m𝒳' : MeasurableSpace 𝒳'}
{μ : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel 𝒳 𝒳')
(η : ProbabilityTheory.Kernel 𝒳 𝒳')
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
ProbabilityTheory.fDiv f (μ.bind ⇑κ) (μ.bind ⇑η) ≤ ProbabilityTheory.fDiv f (μ.compProd κ) (μ.compProd η)