Theorems · Theorem · probability

ProbabilityTheory.HasCondDistrib.comp_right

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

Defined in

Mathlib.Probability.HasCondDistrib

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SFiniteProbabilityTheory.IsSFiniteKernel