Theorems · Theorem · probability

ProbabilityTheory.Kernel.parallelComp_comp_prod

∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {κ : ProbabilityTheory.Kernel X Y} {Y' : Type u_6} {Z' : Type u_7} {mY' : MeasurableSpace Y'}
  {mZ' : MeasurableSpace Z'} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel Y Z}
  [ProbabilityTheory.IsSFiniteKernel η] {κ' : ProbabilityTheory.Kernel X Y'} [ProbabilityTheory.IsSFiniteKernel κ']
  {η' : ProbabilityTheory.Kernel Y' Z'} [ProbabilityTheory.IsSFiniteKernel η'],
  (η.parallelComp η').comp (κ.prod κ') = (η.comp κ).prod (η'.comp κ')

Defined in

Mathlib.Probability.Kernel.Composition.KernelLemmas

Cited by

3 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel