Theorems · Theorem · probability

ProbabilityTheory.Kernel.prod_prodMkRight_comp_deterministic_prod

∀ {β : 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.prodMkRight β η)).comp ((ProbabilityTheory.Kernel.deterministic f hf).prod κ) =
    (ξ.comp ((ProbabilityTheory.Kernel.deterministic f hf).prod κ)).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 η.prodMkRight β for a kernel η. If κ was deterministic, this would be true even if η.prodMkRight β 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

1 results in Mathlib

Foundations

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

Assumes

ProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernelProbabilityTheory.IsSFiniteKernel