Lemmas about the Kullback-Leibler divergence of the images of two measures by a measurable map #
theorem
MeasureTheory.Measure.map_compProd_comap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : Measure α)
[SFinite μ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsSFiniteKernel η]
{f : α → β}
(hf : Measurable f)
:
Transporting μ ⊗ₘ η.comap f along f in the first coordinate gives μ.map f ⊗ₘ η.
theorem
MeasureTheory.Measure.map_withDensity_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{ν : Measure α}
{f : β → ENNReal}
(hf : Measurable f)
{g : α → β}
(hg : Measurable g)
:
theorem
InformationTheory.klDiv_withDensity_comp_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure ν]
{f : β → ENNReal}
(hf : Measurable f)
{g : α → β}
(hg : Measurable g)
[MeasureTheory.IsFiniteMeasure (ν.withDensity (f ∘ g))]
:
klDiv (MeasureTheory.Measure.map g (ν.withDensity (f ∘ g))) (MeasureTheory.Measure.map g ν) = klDiv (ν.withDensity (f ∘ g)) ν
theorem
InformationTheory.klDiv_map_of_eq_withDensity_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
{f : β → ENNReal}
(hf : Measurable f)
{g : α → β}
(hg : Measurable g)
(hμ : μ = ν.withDensity (f ∘ g))
:
If μ has density f ∘ g with respect to ν, then the divergence of the images by g is
the divergence of μ and ν: g is a sufficient statistic.
theorem
InformationTheory.klDiv_compProd_comap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
{f : α → β}
(hf : Measurable f)
:
The conditional divergence of two kernels which depend on the conditioning variable only
through a statistic f is the conditional divergence given f.