Theorems · Theorem · probability

ProbabilityTheory.HasCondDistrib.comp_left

∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {𝓩 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} {Y : Ω → 𝓨}
  {κ : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.SFinite P] [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.HasCondDistrib Y X κ P →
    ∀ {f : 𝓨 → 𝓩}, Measurable f → ProbabilityTheory.HasCondDistrib (f ∘ Y) X (κ.map f) P

Defined in

Mathlib.Probability.HasCondDistrib

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SFiniteProbabilityTheory.IsSFiniteKernel