quasiMeasurePreserving_of_measurable

English

If X is a measurable function and HasPDF X ℙ μ, then X is quasi-measure-preserving from (Ω, ℙ) to (E, μ).

Русский

Если X измерима и HasPDF X ℙ μ, то X является квази-измеримо-представляющим отображение из (Ω, ℙ) в (E, μ).

LaTeX

$$$(\\text{HasPDF } X \\ℙ μ) \\Rightarrow \\text{QuasiMeasurePreserving } X \\ℙ μ$$$

Lean4

/-- A random variable that `HasPDF` is quasi-measure-preserving. -/
theorem quasiMeasurePreserving_of_measurable (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E) [HasPDF X ℙ μ]
    (h : Measurable X) : QuasiMeasurePreserving X ℙ μ :=
  { measurable := h
    absolutelyContinuous := HasPDF.absolutelyContinuous .. }

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