Theorems · Theorem · probability

ProbabilityTheory.posterior_posterior

∀ {Ω : 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 : StandardBorelSpace 𝓧] [inst_5 : Nonempty 𝓧]
  [ProbabilityTheory.IsMarkovKernel κ],
  ⇑(ProbabilityTheory.posterior (ProbabilityTheory.posterior κ μ) (μ.bind ⇑κ)) =ᵐ[μ] ⇑κ

The posterior is involutive (up to μ-a.e. equality).

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.IsMarkovKernel