Theorems · Theorem · probability

ProbabilityTheory.ae_eq_posterior_of_compProd_eq_swap_comp

∀ {Ω : 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 Ω] (η : ProbabilityTheory.Kernel 𝓧 Ω)
  [ProbabilityTheory.IsFiniteKernel η],
  (μ.bind ⇑κ).compProd η = (μ.compProd κ).bind ⇑(ProbabilityTheory.Kernel.swap Ω 𝓧) →
    ⇑η =ᵐ[μ.bind ⇑κ] ⇑(ProbabilityTheory.posterior κ μ)

The posterior is unique up to a κ ∘ₘ μ-null set.

Defined in

Mathlib.Probability.Kernel.Posterior

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureProbabilityTheory.IsFiniteKernelStandardBorelSpaceNonemptyProbabilityTheory.IsFiniteKernel