Theorems · Theorem · probability

ProbabilityTheory.posterior_eq_withDensity_of_countable

∀ {𝓧 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {Ω : Type u_5} [Countable Ω] [inst : MeasurableSpace Ω] [inst_1 : Nonempty Ω]
  [inst_2 : StandardBorelSpace Ω] (κ : ProbabilityTheory.Kernel Ω 𝓧) [inst_3 : ProbabilityTheory.IsFiniteKernel κ]
  (μ : MeasureTheory.Measure Ω) [inst_4 : MeasureTheory.IsFiniteMeasure μ],
  ∀ᵐ (x : 𝓧) ∂μ.bind ⇑κ, (ProbabilityTheory.posterior κ μ) x = μ.withDensity fun ω => (κ ω).rnDeriv (μ.bind ⇑κ) x

Defined in

Mathlib.Probability.Kernel.Posterior

Cited by

2 results in Mathlib

Foundations

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

Assumes

CountableMeasurableSpaceNonemptyStandardBorelSpaceProbabilityTheory.IsFiniteKernelMeasureTheory.IsFiniteMeasure