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 ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η).

If α is countable or β is countably generated, the kernels have a Radon-Nikodym derivative ∂κ/∂η and we give statements in terms of ∂κ/∂η.

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 ∂μ/∂ν.
• rnDeriv_measure_compProd: the Radon-Nikodym derivative ∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η) equals the product of ∂μ/∂ν and ∂κ/∂η.
• rnDeriv_measure_compProd_right: the Radon-Nikodym derivative ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η) (with the same measure) equals ∂κ/∂η.

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 η] : ((ν.withDensity (μ.rnDeriv ν)).compProd κ).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η] (μ.compProd κ).rnDeriv (ν.compProd η)

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 κ] : (μ.compProd κ).rnDeriv (ν.compProd κ) =ᵐ[ν.compProd κ] fun (p : α × β) => μ.rnDeriv ν p.1

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 ν] : (μ.compProd κ).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η] fun (p : α × β) => μ.rnDeriv ν p.1 * (μ.compProd κ).rnDeriv (μ.compProd η) p

The Radon-Nikodym derivative ∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η) equals the product of ∂μ/∂ν and ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η).

See rnDeriv_measure_compProd for a version that replaces ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η) by ∂κ/∂η and does not require the absolute continuity hypothesis, assuming that α is countable or β is countably generated.

theorem ProbabilityTheory.rnDeriv_measure_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ ν : MeasureTheory.Measure α) (κ η : Kernel α β) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [IsFiniteKernel κ] [IsFiniteKernel η] : (μ.compProd κ).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η] fun (p : α × β) => μ.rnDeriv ν p.1 * κ.rnDeriv η p.1 p.2

The Radon-Nikodym derivative ∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η) equals the product of ∂μ/∂ν and ∂κ/∂η.

theorem ProbabilityTheory.rnDeriv_measure_compProd_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (κ η : Kernel α β) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] : (μ.compProd κ).rnDeriv (μ.compProd η) =ᵐ[μ.compProd η] fun (p : α × β) => κ.rnDeriv η p.1 p.2

The Radon-Nikodym derivative ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η) (with the same measure) equals ∂κ/∂η.