Theorems · Theorem · probability

ProbabilityTheory.Kernel.compProd_def

∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ),
  κ.compProd η =
    (((((ProbabilityTheory.Kernel.swap γ β).comp (η.parallelComp ProbabilityTheory.Kernel.id)).comp
                  (ProbabilityTheory.Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯)).comp
              (ProbabilityTheory.Kernel.id.parallelComp (ProbabilityTheory.Kernel.copy β))).comp
          (ProbabilityTheory.Kernel.id.parallelComp κ)).comp
      (ProbabilityTheory.Kernel.copy α)

Defined in

Mathlib.Probability.Kernel.Composition.CompProd

Cited by

5 results in Mathlib

Foundations

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