Theorems · Definition · probability

ProbabilityTheory.posterior

{Ω : Type u_1} →
  {𝓧 : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      {m𝓧 : MeasurableSpace 𝓧} →
        [StandardBorelSpace Ω] →
          [Nonempty Ω] →
            (κ : ProbabilityTheory.Kernel Ω 𝓧) →
              (μ : MeasureTheory.Measure Ω) →
                [MeasureTheory.IsFiniteMeasure μ] → [ProbabilityTheory.IsFiniteKernel κ] → ProbabilityTheory.Kernel 𝓧 Ω

Posterior of the kernel κ with respect to the measure μ.

Defined in

Mathlib.Probability.Kernel.Posterior

Cited by

30 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyMeasureTheory.IsFiniteMeasureProbabilityTheory.IsFiniteKernel