map

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ProbabilityMeasure.map

Lean4

/-- The push-forward of a probability measure by a measurable function. -/
noncomputable def map (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) : ProbabilityMeasure Ω' :=
  ⟨(ν : Measure Ω).map f,
    ⟨by simp only [Measure.map_apply_of_aemeasurable f_aemble MeasurableSet.univ, preimage_univ, measure_univ]⟩⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru