Theorems · Theorem · probability

ProbabilityTheory.Kernel.parallelComp_def

∀ {α : Type u_5} {β : Type u_6} {γ : Type u_7} {δ : Type u_8} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  (η : ProbabilityTheory.Kernel γ δ),
  κ.parallelComp η =
    if h : ProbabilityTheory.IsSFiniteKernel κ ∧ ProbabilityTheory.IsSFiniteKernel η then
      { toFun := fun x => (κ x.1).prod (η x.2), measurable' := ⋯ }
    else 0

Defined in

Mathlib.Probability.Kernel.Composition.ParallelComp

Cited by

3 results in Mathlib

Foundations

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