Theorems · Definition · probability

ProbabilityTheory.condExpKernel

{Ω : Type u_3} →
  [mΩ : MeasurableSpace Ω] →
    [StandardBorelSpace Ω] →
      (μ : MeasureTheory.Measure Ω) →
        [MeasureTheory.IsFiniteMeasure μ] → (m : MeasurableSpace Ω) → ProbabilityTheory.Kernel Ω Ω

Kernel associated with the conditional expectation with respect to a σ-algebra. It satisfies μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condExpKernel μ m ω). It is defined as the conditional distribution of the identity given the identity, where the second identity is understood as a map from Ω with the σ-algebra mΩ to Ω with σ-algebra m ⊓ mΩ. We use m ⊓ mΩ instead of m to ensure that it is a sub-σ-algebra of mΩ. We then use Kernel.comap to get a kernel from m to mΩ instead of from m ⊓ mΩ to mΩ.

Defined in

Mathlib.Probability.Kernel.Condexp

Cited by

49 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceMeasureTheory.IsFiniteMeasure