aemeasurable_of_pdf_ne_zero — Mathlib

English

If the pdf X ℙ μ is not almost everywhere zero, then X is AEMeasurable.

Русский

Если плотность pdf X ℙ μ не равна нулю почти наверняка, тогда X является AEMeasurable.

LaTeX

$$$\\lnot (pdf X \\ℙ μ =ᵐ[μ] 0) \\Rightarrow AEMeasurable X \\ℙ$$$

Lean4

theorem aemeasurable_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} (X : Ω → E)
    (h : ¬pdf X ℙ μ =ᵐ[μ] 0) : AEMeasurable X ℙ := by
  contrapose! h
  exact pdf_of_not_aemeasurable h

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