quasiMeasurePreserving_hasPDF' — Mathlib

English

For a random variable X, HasPDF X ℙ holds if and only if X is ae-measurable and the push-forward measure X♯ℙ is absolutely continuous with respect to Lebesgue measure.

Русский

Для случайной величины X выполнение HasPDF X ℙ эквивалентно тому, что X измерима почти во всех точках и образующая мера X♯ℙ абсолютно непрерывна по отношению к объёму.

LaTeX

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

Lean4

theorem quasiMeasurePreserving_hasPDF' [SFinite ℙ] [SigmaFinite ν] (hg : QuasiMeasurePreserving g μ ν) :
    HasPDF (g ∘ X) ℙ ν :=
  quasiMeasurePreserving_hasPDF X hg inferInstance

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