hasPDF_of_pdf_ne_zero — Mathlib

English

If map X ℙ is absolutely continuous wrt μ and pdf X ℙ μ ≠ᵐ[μ] 0, then HasPDF X ℙ μ.

Русский

Если map X ℙ абсолютно непрерывна по μ и pdf X ℙ μ ≠ 0 почти наверняка, то HasPDF X ℙ μ.

LaTeX

$$$(Map X \\ℙ) \\ll μ \\land pdf X \\ℙ μ ≠ᵐ[μ] 0 \\Rightarrow HasPDF X \\ℙ μ$$$

Lean4

theorem hasPDF_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} (hac : map X ℙ ≪ μ)
    (hpdf : ¬pdf X ℙ μ =ᵐ[μ] 0) : HasPDF X ℙ μ :=
  by
  refine ⟨?_, ?_, hac⟩
  · exact aemeasurable_of_pdf_ne_zero X hpdf
  · contrapose! hpdf
    have := pdf_of_not_haveLebesgueDecomposition hpdf
    filter_upwards using congrFun this

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