absolutelyContinuous

Mathlib.Probability.Density

URI: https://scilib.ai/kg/mathlib#MeasureTheory.HasPDF.absolutelyContinuous

English

If X has a PDF, then the pushforward measure map X ℙ is absolutely continuous with respect to μ.

Русский

Если у X есть плотность, то образующая мера map X ℙ абсолютно непрерывна относительно μ.

LaTeX

$$$map X \\ℙ \\ll μ$$$

Lean4

theorem absolutelyContinuous [HasPDF X ℙ μ] : map X ℙ ≪ μ :=
  HasPDF.absolutelyContinuous'

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

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

Разделы

Аффилиация

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