Radon-Nikodym derivative of a composition product #
We compute the Radon-Nikodym derivative of a composition product μ ⊗ₘ κ with respect to another
composition product ν ⊗ₘ η in terms of the Radon-Nikodym derivatives ∂μ/∂ν and
∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η).
Main statements #
rnDeriv_compProd: the Radon-Nikodym derivative∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)equals the product of∂μ/∂νand∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η).rnDeriv_measure_compProd_left: the Radon-Nikodym derivative∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ κ)(with the same kernel) equals∂μ/∂ν.
TODO #
Under suitable assumptions to have Radon-Nikodym derivatives defined for kernels, we should give
equivalent statements with ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η) replaced by ∂κ/∂η.
theorem
ProbabilityTheory.rnDeriv_compProd_withDensity_rnDeriv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ ν : MeasureTheory.Measure α)
(κ η : Kernel α β)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
[IsFiniteKernel κ]
[IsFiniteKernel η]
:
Auxiliary lemma for rnDeriv_measure_compProd_left.
theorem
ProbabilityTheory.rnDeriv_measure_compProd_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ ν : MeasureTheory.Measure α)
(κ : Kernel α β)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
[IsFiniteKernel κ]
:
The Radon-Nikodym derivative ∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ κ) (with the same kernel) equals ∂μ/∂ν.
theorem
ProbabilityTheory.rnDeriv_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ η : Kernel α β}
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
[IsFiniteKernel η]
(h_ac : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η))
(ν : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure ν]
:
The Radon-Nikodym derivative ∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η) equals the product of ∂μ/∂ν and
∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η).