Theorems · Definition · probability

ProbabilityTheory.Kernel.condKernel

{α : Type u_5} →
  {β : Type u_6} →
    {Ω : Type u_7} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} →
          {mΩ : MeasurableSpace Ω} →
            [StandardBorelSpace Ω] →
              [Nonempty Ω] →
                [h : MeasurableSpace.CountableOrCountablyGenerated α β] →
                  (κ : ProbabilityTheory.Kernel α (β × Ω)) →
                    [ProbabilityTheory.IsFiniteKernel κ] → ProbabilityTheory.Kernel (α × β) Ω

Conditional kernel of a kernel κ : Kernel α (β × Ω): a Markov kernel such that fst κ ⊗ₖ condKernel κ = κ (see MeasureTheory.Measure.compProd_fst_condKernel). It exists whenever Ω is standard Borel and either α is countable or β is countably generated.

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

16 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyMeasurableSpace.CountableOrCountablyGeneratedProbabilityTheory.IsFiniteKernel