Theorems · Definition · probability

MeasureTheory.Measure.condKernel

{α : Type u_5} →
  {Ω : Type u_6} →
    {mα : MeasurableSpace α} →
      {mΩ : MeasurableSpace Ω} →
        [StandardBorelSpace Ω] →
          [Nonempty Ω] →
            (ρ : MeasureTheory.Measure (α × Ω)) → [MeasureTheory.IsFiniteMeasure ρ] → ProbabilityTheory.Kernel α Ω

Conditional kernel of a measure on a product space: a Markov kernel such that ρ = ρ.fst ⊗ₘ ρ.condKernel (see MeasureTheory.Measure.compProd_fst_condKernel).

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

38 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyMeasureTheory.IsFiniteMeasure