ofReal_toReal_ae_eq — Mathlib

English

If μ is finite, then the a.e. equality between pdf values and their real-valued counterparts holds after applying ofReal toReal.

Русский

Если μ конечно, то равенство почти всюду между pdf и их вещественными эквивалентами сохраняется после применения ofReal.

LaTeX

$$$(fun x \\mapsto ENNReal.ofReal (pdf X ℙ μ x).toReal) =ᵐ[μ] pdf X ℙ μ$$$

Lean4

nonrec theorem ofReal_toReal_ae_eq [IsFiniteMeasure ℙ] {X : Ω → E} :
    (fun x => ENNReal.ofReal (pdf X ℙ μ x).toReal) =ᵐ[μ] pdf X ℙ μ :=
  ofReal_toReal_ae_eq ae_lt_top

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