Theorems · Theorem · probability

ProbabilityTheory.deterministic_comp_posterior

∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure Ω}
  [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [MeasurableSpace.CountablyGenerated 𝓧] {f : Ω → 𝓧} (hf : Measurable f),
  ⇑((ProbabilityTheory.Kernel.deterministic f hf).comp
        (ProbabilityTheory.posterior (ProbabilityTheory.Kernel.deterministic f hf) μ)) =ᵐ[MeasureTheory.Measure.map f μ]
    ⇑ProbabilityTheory.Kernel.id

For a deterministic kernel κ, κ ∘ₖ κ†μ is μ.map f-a.e. equal to the identity kernel.

Defined in

Mathlib.Probability.Kernel.Posterior

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureStandardBorelSpaceNonemptyMeasurableSpace.CountablyGenerated