Theorems · Definition · measure theory

MeasureTheory.ProbabilityMeasure.map

{Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] →
        (ν : MeasureTheory.ProbabilityMeasure Ω) →
          {f : Ω → Ω'} → AEMeasurable f ↑ν → MeasureTheory.ProbabilityMeasure Ω'

The push-forward of a probability measure by a measurable function.

Defined in

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Cited by

12 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace