Theorems · Theorem · measure theory

MeasureTheory.lintegral_rnDeriv_compProd

∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨}
  {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsFiniteKernel η],
  (μ.compProd κ).AbsolutelyContinuous (μ.compProd η) →
    ∀ᵐ (a : 𝓧) ∂μ, ∫⁻ (b : 𝓨), (μ.compProd κ).rnDeriv (μ.compProd η) (a, b) ∂η a = (κ a) Set.univ

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsFiniteKernel