Theorems · Theorem · probability

ProbabilityTheory.Kernel.comp_parallelComp_comp_copy

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_3}
  [inst : MeasurableSpace γ] {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ}
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η]
  [ProbabilityTheory.IsDeterministic (η.comp κ)],
  ((η.comp κ).parallelComp κ).comp (ProbabilityTheory.Kernel.copy α) =
    ((η.parallelComp ProbabilityTheory.Kernel.id).comp (ProbabilityTheory.Kernel.copy β)).comp κ

The equation of a Positive Markov category: if the composition of two Markov kernels η ∘ₖ κ is deterministic, the distribution over both η ∘ₖ κ and κ can be obtained by computing η ∘ₖ κ and κ independently.

Defined in

Mathlib.Probability.Kernel.Deterministic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceProbabilityTheory.IsMarkovKernelProbabilityTheory.IsMarkovKernelProbabilityTheory.IsDeterministic