Theorems · Definition · probability

ProbabilityTheory.Kernel.singularPart

{α : Type u_3} →
  {γ : Type u_4} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] →
          (κ η : ProbabilityTheory.Kernel α γ) →
            [ProbabilityTheory.IsSFiniteKernel κ] → [ProbabilityTheory.IsSFiniteKernel η] → ProbabilityTheory.Kernel α γ

Singular part of the kernel κ with respect to the kernel η.

Defined in

Mathlib.Probability.Kernel.RadonNikodym

Cited by

17 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountableOrCountablyGeneratedProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel