Composition of kernels and measures with density #
We prove lemmas about Kernel.withDensity and Measure.withDensity in relation with the
composition of kernels and measures.
theorem
MeasureTheory.Measure.withDensity_comp
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{μ : Measure 𝓧}
{κ : ProbabilityTheory.Kernel 𝓧 𝓨}
[ProbabilityTheory.IsSFiniteKernel κ]
{f' : 𝓨 → ENNReal}
(hf' : Measurable f')
:
theorem
MeasureTheory.Measure.compProd_withDensity
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{μ : Measure 𝓧}
{κ : ProbabilityTheory.Kernel 𝓧 𝓨}
[ProbabilityTheory.IsSFiniteKernel κ]
{g : 𝓧 → 𝓨 → ENNReal}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel (κ.withDensity g)]
(hg : Measurable (Function.uncurry g))
:
A composition-product of a measure with a kernel defined with withDensity is equal to the
withDensity of the composition-product.
theorem
MeasureTheory.Measure.withDensity_compProd
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{μ : Measure 𝓧}
{κ : ProbabilityTheory.Kernel 𝓧 𝓨}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : 𝓧 → ENNReal}
[SFinite μ]
(hf : Measurable f)
:
theorem
MeasureTheory.Measure.withDensity_compProd_withDensity
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{μ : Measure 𝓧}
{κ : ProbabilityTheory.Kernel 𝓧 𝓨}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : 𝓧 → ENNReal}
{g : 𝓧 → 𝓨 → ENNReal}
[SFinite μ]
[ProbabilityTheory.IsSFiniteKernel (κ.withDensity g)]
(hf : Measurable f)
(hg : Measurable (Function.uncurry g))
:
(μ.withDensity f).compProd (κ.withDensity g) = (μ.compProd κ).withDensity fun (ac : 𝓧 × 𝓨) => f ac.1 * g ac.1 ac.2
theorem
ProbabilityTheory.Kernel.withDensity_comp_left
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{𝓩 : Type u_3}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{κ : Kernel 𝓧 𝓨}
[IsSFiniteKernel κ]
{η : Kernel 𝓨 𝓩}
[IsSFiniteKernel η]
{f : 𝓧 → ENNReal}
(hf : Measurable f)
:
((η.comp κ).withDensity fun (a : 𝓧) (x : 𝓩) => f a) = η.comp (κ.withDensity fun (a : 𝓧) (x : 𝓨) => f a)
theorem
ProbabilityTheory.Kernel.withDensity_comp_right
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{𝓩 : Type u_3}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{κ : Kernel 𝓧 𝓨}
[IsSFiniteKernel κ]
{η : Kernel 𝓨 𝓩}
[IsSFiniteKernel η]
{f : 𝓩 → ENNReal}
(hf : Measurable f)
:
((η.comp κ).withDensity fun (x : 𝓧) (z : 𝓩) => f z) = (η.withDensity fun (x : 𝓨) (z : 𝓩) => f z).comp κ
theorem
ProbabilityTheory.Kernel.sectR_withDensity
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{𝓩 : Type u_3}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{η : Kernel (𝓧 × 𝓨) 𝓩}
[IsSFiniteKernel η]
{g : 𝓧 × 𝓨 → 𝓩 → ENNReal}
(hg : Measurable (Function.uncurry g))
(a : 𝓧)
:
theorem
ProbabilityTheory.Kernel.compProd_withDensity
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{𝓩 : Type u_3}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{κ : Kernel 𝓧 𝓨}
[IsSFiniteKernel κ]
{η : Kernel (𝓧 × 𝓨) 𝓩}
[IsSFiniteKernel η]
{g : 𝓧 × 𝓨 → 𝓩 → ENNReal}
(hg : Measurable (Function.uncurry g))
[IsSFiniteKernel (η.withDensity g)]
:
κ.compProd (η.withDensity g) = (κ.compProd η).withDensity fun (a : 𝓧) (bc : 𝓨 × 𝓩) => g (a, bc.1) bc.2
theorem
ProbabilityTheory.Kernel.withDensity_compProd
{𝓧 : Type u_1}
{𝓨 : Type u_2}
{𝓩 : Type u_3}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{κ : Kernel 𝓧 𝓨}
[IsSFiniteKernel κ]
{g : 𝓧 → 𝓨 → ENNReal}
{η : Kernel (𝓧 × 𝓨) 𝓩}
[IsSFiniteKernel η]
[IsSFiniteKernel (κ.withDensity g)]
(hg : Measurable (Function.uncurry g))
: