eq_of_map_eq_withDensity — Mathlib

English

If X has a finite measure P and hasPDF X ℙ μ, then map X ℙ = μ.withDensity f if and only if pdf X ℙ μ =ᵐ[μ] f, for any density f.

Русский

Если X имеет конечную меру и 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 [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] (f : E → ℝ≥0∞)
    (hmf : AEMeasurable f μ) : map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᵐ[μ] f :=
  by
  rw [map_eq_withDensity_pdf X ℙ μ]
  apply withDensity_eq_iff (measurable_pdf X ℙ μ).aemeasurable hmf
  rw [lintegral_eq_measure_univ]
  exact measure_ne_top _ _

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