aemeasurable

Mathlib.Probability.Density

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

English

If X has a pdf with respect to ℙ and μ, then X is AEMeasurable with respect to ℙ.

Русский

Если X имеет плотность относительно ℙ и μ, то X является AEMeasurable относительно ℙ.

LaTeX

$$$HasPDF X \\ℙ μ \\implies AEMeasurable X \\ℙ$$$

Lean4

@[measurability]
theorem aemeasurable [HasPDF X ℙ μ] : AEMeasurable X ℙ :=
  HasPDF.aemeasurable' μ

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

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

Разделы

Аффилиация

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