Theorems · Definition · probability

ProbabilityTheory.Kernel.condKernelBorel

{α : Type u_1} →
  {γ : Type u_3} →
    {Ω : Type u_4} →
      {mα : MeasurableSpace α} →
        {mγ : MeasurableSpace γ} →
          [MeasurableSpace.CountablyGenerated γ] →
            {mΩ : MeasurableSpace Ω} →
              [StandardBorelSpace Ω] →
                [Nonempty Ω] →
                  (κ : ProbabilityTheory.Kernel α (γ × Ω)) →
                    [ProbabilityTheory.IsFiniteKernel κ] → ProbabilityTheory.Kernel (α × γ) Ω

Auxiliary definition for ProbabilityTheory.Kernel.condKernel. A conditional kernel for κ : Kernel α (γ × Ω) where γ is countably generated and Ω is standard Borel.

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountablyGeneratedStandardBorelSpaceNonemptyProbabilityTheory.IsFiniteKernel