Theorems · Definition · probability

ProbabilityTheory.Kernel.condKernelUnitBorel

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

Auxiliary definition for MeasureTheory.Measure.condKernel and ProbabilityTheory.Kernel.condKernel. A conditional kernel for κ : Kernel Unit (α × Ω) where Ω is standard Borel.

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

3 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyProbabilityTheory.IsFiniteKernel