Theorems · Definition · probability

ProbabilityTheory.Kernel.withDensity

{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (κ : ProbabilityTheory.Kernel α β) →
          [ProbabilityTheory.IsSFiniteKernel κ] → (α → β → ENNReal) → ProbabilityTheory.Kernel α β

Kernel with image (κ a).withDensity (f a) if Function.uncurry f is measurable, and with image 0 otherwise. If Function.uncurry f is measurable, it satisfies ∫⁻ b, g b ∂(withDensity κ f hf a) = ∫⁻ b, f a b * g b ∂(κ a).

Defined in

Mathlib.Probability.Kernel.WithDensity

Cited by

45 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsSFiniteKernel