Theorems · Theorem · probability

ProbabilityTheory.HasCondDistrib.of_compProd

∀ {Ω : 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 κ] {Z : Ω → 𝓩}
  {η : ProbabilityTheory.Kernel (𝓧 × 𝓨) 𝓩} [ProbabilityTheory.IsMarkovKernel η],
  ProbabilityTheory.HasCondDistrib (fun a => (Y a, Z a)) X (κ.compProd η) P →
    ProbabilityTheory.HasCondDistrib Z (fun a => (X a, Y a)) η P

Defined in

Mathlib.Probability.HasCondDistrib

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SFiniteProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsMarkovKernel