uniformPDF_eq_pdf — Mathlib

English

For measurable s, if X is Uniform on s, then the pdf equals the uniform density almost everywhere.

Русский

Для измеримого s, если X равномерно распределён на s, то pdf совпадает с однородной плотностью почти наверняка.

LaTeX

$$$\\text{pdf}(X,\\mathbb{P},\\mu)=^a_e \\text{uniformPDF}(s,\\mu)$ при измеримости s$$

Lean4

/-- Check that indeed any uniform random variable has the uniformPDF. -/
theorem uniformPDF_eq_pdf {s : Set E} (hs : MeasurableSet s) (hu : pdf.IsUniform X s ℙ μ) :
    (fun x ↦ uniformPDF s x μ) =ᵐ[μ] pdf X ℙ μ := by
  unfold uniformPDF
  exact Filter.EventuallyEq.trans (pdf.IsUniform.pdf_eq hs hu).symm (ae_eq_refl _)

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