Theorems · Theorem · probability

ProbabilityTheory.HasCondDistrib.snd

∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {𝓩 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} [MeasureTheory.SFinite P]
  {Y : Ω → 𝓨 × 𝓩} {κ : ProbabilityTheory.Kernel 𝓧 (𝓨 × 𝓩)} [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.HasCondDistrib Y X κ P → ProbabilityTheory.HasCondDistrib (fun ω => (Y ω).2) X κ.snd P

Defined in

Mathlib.Probability.HasCondDistrib

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SFiniteProbabilityTheory.IsSFiniteKernel