Theorems · Theorem · probability

ProbabilityTheory.Kernel.prod_prodMkLeft_comp_prod_deterministic

∀ {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} {β' : Type u_5} {ε : Type u_6} {mβ' : MeasurableSpace β'} {mε : MeasurableSpace ε}
  (κ : ProbabilityTheory.Kernel γ β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel ε β')
  [ProbabilityTheory.IsSFiniteKernel η] (ξ : ProbabilityTheory.Kernel (β × ε) δ) [ProbabilityTheory.IsSFiniteKernel ξ]
  {f : γ → ε} (hf : Measurable f),
  (ξ.prod (ProbabilityTheory.Kernel.prodMkLeft β η)).comp (κ.prod (ProbabilityTheory.Kernel.deterministic f hf)) =
    (ξ.comp (κ.prod (ProbabilityTheory.Kernel.deterministic f hf))).prod
      (η.comp (ProbabilityTheory.Kernel.deterministic f hf))

The composition of two product kernels (ξ ×ₖ η') ∘ₖ (κ ×ₖ ζ) is the product of the compositions (ξ ∘ₖ (κ ×ₖ ζ)) ×ₖ (η' ∘ₖ (κ ×ₖ ζ)), if ζ is deterministic (of the form .deterministic f hf) and η' does not depend on the output of κ. That is, η' has the form η.prodMkLeft β for a kernel η. If κ was deterministic, this would be true even if η.prodMkLeft β was a more general kernel since κ ×ₖ Kernel.deterministic f hf would be deterministic and commute with copying. Here κ is not deterministic, but it is discarded in one branch of the copy.

Defined in

Mathlib.Probability.Kernel.Composition.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel