hasPDF_iff — Mathlib

English

If X is AE-measurable, then HasPDF X ℙ iff the push-forward is absolutely continuous with Lebesgue measure.

Русский

Если X измерима почти везде, тогда HasPDF X ℙ эквивалентно тому, что образующая мера принадлежит к Absolutely Continuous по отношению к объёму.

LaTeX

$$$\text{HasPDF}(X,\mathbb{P}) \iff (\mathbb{P}\circ X^{-1}) \ll \mathrm{volume}.$$$

Lean4

nonrec theorem _root_.Real.hasPDF_iff [SFinite ℙ] : HasPDF X ℙ ↔ AEMeasurable X ℙ ∧ map X ℙ ≪ volume := by
  rw [hasPDF_iff, and_iff_right (inferInstance : HaveLebesgueDecomposition _ _)]

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