Radon-Nikodym derivative of the composition of a measure and a kernel #
theorem
ProbabilityTheory.toReal_rnDeriv_comp_eq_condexp_compProd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(hκη : ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x))
:
(fun (ab : α × β) => ((μ.bind ⇑κ).rnDeriv (ν.bind ⇑η) ab.2).toReal) =ᵐ[ν.compProd η] MeasureTheory.condexp (MeasurableSpace.comap Prod.snd mβ) (ν.compProd η) fun (ab : α × β) =>
((μ.compProd κ).rnDeriv (ν.compProd η) ab).toReal
theorem
ProbabilityTheory.toReal_rnDeriv_comp_eq_condexp_compProd_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
:
(fun (ab : α × β) => ((μ.bind ⇑κ).rnDeriv (ν.bind ⇑κ) ab.2).toReal) =ᵐ[ν.compProd κ] MeasureTheory.condexp (MeasurableSpace.comap Prod.snd mβ) (ν.compProd κ) fun (ab : α × β) =>
((μ.compProd κ).rnDeriv (ν.compProd κ) ab).toReal
theorem
ProbabilityTheory.toReal_rnDeriv_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hμν : μ.AbsolutelyContinuous ν)
[ProbabilityTheory.IsFiniteKernel κ]
:
(fun (ab : α × β) => ((μ.bind ⇑κ).rnDeriv (ν.bind ⇑κ) ab.2).toReal) =ᵐ[ν.compProd κ] MeasureTheory.condexp (MeasurableSpace.comap Prod.snd mβ) (ν.compProd κ) fun (ab : α × β) => (μ.rnDeriv ν ab.1).toReal
theorem
Measurable.setLIntegral_kernel_prod_right'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α × β → ENNReal}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
Measurable fun (a : α) => ∫⁻ (b : β) in s, f (a, b) ∂κ a