Theorems · Definition · probability

ProbabilityTheory.Kernel.mutuallySingularSetSlice

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

A set of points in α × γ related to the absolute continuity / mutual singularity of κ and η. That is, * withDensity η (rnDeriv κ η) a (mutuallySingularSetSlice κ η a) = 0, * singularPart κ η a (mutuallySingularSetSlice κ η a)ᶜ = 0.

Defined in

Mathlib.Probability.Kernel.RadonNikodym

Cited by

19 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountableOrCountablyGenerated