Theorems · Definition · probability

ProbabilityTheory.Kernel.density

{α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} →
            [MeasurableSpace.CountablyGenerated γ] →
              ProbabilityTheory.Kernel α (γ × β) → ProbabilityTheory.Kernel α γ → α → γ → Set β → ℝ

Density of the kernel κ with respect to ν. This is a function α → γ → Set β → ℝ which is measurable on α × γ for all measurable sets s : Set β and satisfies that ∫ x in A, density κ ν a x s ∂(ν a) = (κ a).real (A ×ˢ s) for all measurable A : Set γ.

Defined in

Mathlib.Probability.Kernel.Disintegration.Density

Cited by

24 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountablyGenerated