Theorems · Theorem · probability

ProbabilityTheory.parallelProd_posterior_comp_copy_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 Ω],
  ((μ.bind ⇑κ).bind ⇑(ProbabilityTheory.Kernel.copy 𝓧)).bind
      ⇑(ProbabilityTheory.Kernel.id.parallelComp (ProbabilityTheory.posterior κ μ)) =
    (μ.bind ⇑(ProbabilityTheory.Kernel.copy Ω)).bind ⇑(κ.parallelComp ProbabilityTheory.Kernel.id)

The main property of the posterior, as equality of the following diagrams: `` -- id -- κ μ -- κ -| = μ -| -- κ†μ -- id ``

Defined in

Mathlib.Probability.Kernel.Posterior

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureProbabilityTheory.IsFiniteKernelStandardBorelSpaceNonempty