Theorems · Definition · probability

ProbabilityTheory.Kernel.borelMarkovFromReal

{α : Type u_1} →
  {mα : MeasurableSpace α} →
    (Ω : Type u_5) →
      [Nonempty Ω] →
        [inst : MeasurableSpace Ω] →
          [StandardBorelSpace Ω] → ProbabilityTheory.Kernel α ℝ → ProbabilityTheory.Kernel α Ω

Auxiliary definition for ProbabilityTheory.Kernel.condKernel. A Borel space Ω embeds measurably into ℝ (with embedding e), hence we can get a Kernel α Ω from a Kernel α ℝ by taking the comap by e. Here we take the comap of a modification of η : Kernel α ℝ, useful when η a is a probability measure with all its mass on range e almost everywhere with respect to some measure and we want to ensure that the comap is a Markov kernel. We thus take the comap by e of a kernel defined piecewise: η when η a (range (embeddingReal Ω))ᶜ = 0, and an arbitrary deterministic kernel otherwise.

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

5 results in Mathlib

Foundations

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

Assumes

NonemptyMeasurableSpaceStandardBorelSpace