Theorems · Definition · probability

ProbabilityTheory.Kernel.rnDerivAux

{α : Type u_1} →
  {γ : Type u_2} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] →
          ProbabilityTheory.Kernel α γ → ProbabilityTheory.Kernel α γ → α → γ → ℝ

Auxiliary function used to define ProbabilityTheory.Kernel.rnDeriv and ProbabilityTheory.Kernel.singularPart. This has the properties we want for a Radon-Nikodym derivative only if κ ≪ ν. The definition of rnDeriv κ η will be built from rnDerivAux κ (κ + η).

Defined in

Mathlib.Probability.Kernel.RadonNikodym

Cited by

22 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountableOrCountablyGenerated