Theorems · Definition · probability

ProbabilityTheory.Kernel.mapOfMeasurable

{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          {mγ : MeasurableSpace γ} →
            ProbabilityTheory.Kernel α β → (f : β → γ) → Measurable f → ProbabilityTheory.Kernel α γ

The pushforward of a kernel along a measurable function. This is an implementation detail, use map κ f instead.

Defined in

Mathlib.Probability.Kernel.Composition.MapComap

Cited by

4 results in Mathlib

Foundations

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