Theorems · Theorem · probability

ProbabilityTheory.Kernel.singularPart_def

∀ {α : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsSFiniteKernel κ] [inst_1 : ProbabilityTheory.IsSFiniteKernel η],
  κ.singularPart η =
    (κ + η).withDensity fun a x =>
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x

Defined in

Mathlib.Probability.Kernel.RadonNikodym

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountableOrCountablyGeneratedProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel