Theorems · Theorem · probability

ProbabilityTheory.rnDeriv_compProd

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ]
  [ProbabilityTheory.IsFiniteKernel η],
  (μ.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 ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η).

Defined in

Mathlib.Probability.Kernel.Composition.RadonNikodym

Cited by

2 results in Mathlib

Foundations

Depth 233 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasureProbabilityTheory.IsFiniteKernelProbabilityTheory.IsFiniteKernelMeasureTheory.IsFiniteMeasure