Theorems · Definition · probability

ProbabilityTheory.condDistrib

{α : Type u_5} →
  {β : Type u_6} →
    {Ω : Type u_7} →
      [inst : MeasurableSpace Ω] →
        [StandardBorelSpace Ω] →
          [Nonempty Ω] →
            {x : MeasurableSpace α} →
              [inst_3 : MeasurableSpace β] →
                (α → Ω) →
                  (α → β) →
                    (μ : MeasureTheory.Measure α) → [MeasureTheory.IsFiniteMeasure μ] → ProbabilityTheory.Kernel β Ω

Regular conditional probability distribution: kernel associated with the conditional expectation of Y given X. For almost all a, condDistrib Y X μ evaluated at X a and a measurable set s is equal to the conditional expectation μ⟦Y ⁻¹' s | mβ.comap X⟧ a. It also satisfies the equality μ[(fun a => f (X a, Y a)) | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂(condDistrib Y X μ (X a)) for all integrable functions f.

Defined in

Mathlib.Probability.Kernel.CondDistrib

Cited by

58 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyMeasurableSpaceMeasureTheory.IsFiniteMeasure