Theorems · Definition · probability

ProbabilityTheory.Kernel.densityProcess

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

An ℕ-indexed martingale that is a density for κ with respect to ν on the sets in countablePartition γ n. Used to define its limit ProbabilityTheory.Kernel.density, which is a density for those kernels for all measurable sets.

Defined in

Mathlib.Probability.Kernel.Disintegration.Density

Cited by

37 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountablyGenerated