Theorems · Theorem · probability

ProbabilityTheory.posterior_eq_withDensity

∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧],
  (∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)) →
    ∀ᵐ (x : 𝓧) ∂μ.bind ⇑κ,
      (ProbabilityTheory.posterior κ μ) x =
        μ.withDensity fun ω => κ.rnDeriv (ProbabilityTheory.Kernel.const Ω (μ.bind ⇑κ)) ω x

If κ ω ≪ κ ∘ₘ μ for μ-almost every ω, then for κ ∘ₘ μ-almost every x, κ†μ x = μ.withDensity (fun ω ↦ κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) ω x). This is a form of Bayes' theorem. The condition is true for example for countable Ω.

Defined in

Mathlib.Probability.Kernel.Posterior

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureProbabilityTheory.IsFiniteKernelStandardBorelSpaceNonemptyMeasurableSpace.CountableOrCountablyGenerated