pdf_of_not_aemeasurable — Mathlib

English

If X is not AEMeasurable, then pdf X ℙ μ =ᵐ[μ] 0 (zero a.e.).

Русский

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

LaTeX

$$$pdf X \\ℙ μ =ᵐ[μ] 0$$$

Lean4

theorem pdf_of_not_aemeasurable {_ : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E}
    (hX : ¬AEMeasurable X ℙ) : pdf X ℙ μ =ᵐ[μ] 0 :=
  by
  rw [pdf_def, map_of_not_aemeasurable hX]
  exact rnDeriv_zero μ

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