pdf_toReal_ae_eq — Mathlib

English

If X is uniform on s, then the Real-valued version of pdf matches the Real-interpretation of the density a.e.

Русский

Если X равномерна на s, то соответствие pdf в вещественных значениях совпадает почти surely с реальным представлением плотности.

LaTeX

$$$\\text{pdf}_{\\mathbb{R}}(X,\\mathbb{P},\\mu)=^a_e (\\text{indicator}_{s} ( (\\mu s)^{-1} ) )$$$

Lean4

theorem pdf_toReal_ae_eq {X : Ω → E} {s : Set E} (hms : MeasurableSet s) (hX : IsUniform X s ℙ μ) :
    (fun x => (pdf X ℙ μ x).toReal) =ᵐ[μ] fun x => (s.indicator ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) x).toReal :=
  Filter.EventuallyEq.fun_comp (pdf_eq hms hX) ENNReal.toReal

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