Theorems · Definition · probability

ProbabilityTheory.Kernel.compProd

{α : Type u_4} →
  {β : Type u_5} →
    {γ : Type u_6} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mγ : MeasurableSpace γ} →
            ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel (α × β) γ → ProbabilityTheory.Kernel α (β × γ)

Composition-Product of kernels. For s-finite kernels, it satisfies ∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a) (see ProbabilityTheory.Kernel.lintegral_compProd). If either of the kernels is not s-finite, compProd is given the junk value 0.

Defined in

Mathlib.Probability.Kernel.Composition.CompProd

Cited by

99 results in Mathlib

Foundations

Depth 224 from the axioms, rests on 5,398 definitions · uses propext, Classical.choice, Quot.sound