Theorems · Definition · probability

ProbabilityTheory.Kernel.map

{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          [inst : MeasurableSpace γ] → ProbabilityTheory.Kernel α β → (β → γ) → ProbabilityTheory.Kernel α γ

The pushforward of a kernel along a function. If the function is not measurable, we use zero instead. This choice of junk value ensures that typeclass inference can infer that the map of a kernel satisfying IsZeroOrMarkovKernel again satisfies this property.

Defined in

Mathlib.Probability.Kernel.Composition.MapComap

Cited by

84 results in Mathlib

Foundations

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

Assumes

MeasurableSpace