English
A variation of the previous statement: with the same hypothesis, HasPDF is equivalent to push-forward absolutely continuous with Lebesgue measure.
Русский
С теми же предположениями, HasPDF эквивалентно тому, что образующая мера абсолютно непрерывна по отношению к объёму.
LaTeX
$$$\text{HasPDF}(X,\mathbb{P}) \iff (\mathbb{P}\circ X^{-1}) \ll \mathrm{volume}.$$$
Lean4
/-- A real-valued random variable `X` `HasPDF X ℙ λ` (where `λ` is the Lebesgue measure) if and
only if the push-forward measure of `ℙ` along `X` is absolutely continuous with respect to `λ`. -/
nonrec theorem _root_.Real.hasPDF_iff_of_aemeasurable [SFinite ℙ] (hX : AEMeasurable X ℙ) :
HasPDF X ℙ ↔ map X ℙ ≪ volume := by rw [Real.hasPDF_iff, and_iff_right hX]
