Theorems · Theorem · probability

ProbabilityTheory.posterior_comp

∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {κ : ProbabilityTheory.Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω}
  [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ] [inst_2 : StandardBorelSpace Ω]
  [inst_3 : Nonempty Ω] [inst_4 : StandardBorelSpace 𝓧] [inst_5 : Nonempty 𝓧] {η : ProbabilityTheory.Kernel 𝓧 𝓨}
  [inst_6 : ProbabilityTheory.IsFiniteKernel η],
  ⇑(ProbabilityTheory.posterior (η.comp κ) μ) =ᵐ[(μ.bind ⇑κ).bind ⇑η]
    ⇑((ProbabilityTheory.posterior κ μ).comp (ProbabilityTheory.posterior η (μ.bind ⇑κ)))

The posterior is contravariant.

Defined in

Mathlib.Probability.Kernel.Posterior

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureProbabilityTheory.IsFiniteKernelStandardBorelSpaceNonemptyStandardBorelSpaceNonemptyProbabilityTheory.IsFiniteKernel