eq_of_map_eq_withDensity' — Mathlib

English

Under sigma-finite μ, and HasPDF X ℙ μ, map X ℙ = μ.withDensity f iff pdf X ℙ μ =ᵐ[μ] f for any f.

Русский

При σ-конечности μ и HasPDF X ℙ μ, map X ℙ = μ.withDensity f эквивалентно pdf X ℙ μ =ᵐ[μ] f для любой f.

LaTeX

$$$map X \\ℙ = μ.withDensity f \\iff pdf X \\ℙ μ =ᵐ[μ] f$$$

Lean4

theorem eq_of_map_eq_withDensity' [SigmaFinite μ] {X : Ω → E} [HasPDF X ℙ μ] (f : E → ℝ≥0∞) (hmf : AEMeasurable f μ) :
    map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᵐ[μ] f :=
  map_eq_withDensity_pdf X ℙ μ ▸ withDensity_eq_iff_of_sigmaFinite (measurable_pdf X ℙ μ).aemeasurable hmf

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