English
For measurable s and uniform X, pdf X ℙ μ equals the indicator on s scaled by (μ(s))⁻¹ almost everywhere.
Русский
Для измеримого s и равномерного X плотность pdf(X) равна индикатору s, умноженному на (μ(s))⁻¹, почти surely.
LaTeX
$$$\\text{pdf}(X,\\mathbb{P},\\mu)=^a_e s\\,\\mathbf{1}((\mu(s))^{-1}\\,1)$ на s и 0 вне s$$
Lean4
theorem pdf_eq {X : Ω → E} {s : Set E} (hms : MeasurableSet s) (hu : IsUniform X s ℙ μ) :
pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) :=
by
by_cases hnt : μ s = ∞
· simp [pdf_eq_zero_of_measure_eq_zero_or_top hu (Or.inr hnt), hnt]
by_cases hns : μ s = 0
· filter_upwards [measure_eq_zero_iff_ae_notMem.mp hns, pdf_eq_zero_of_measure_eq_zero_or_top hu (Or.inl hns)] with x
hx h'x
simp [hx, h'x, hns]
have : HasPDF X ℙ μ := hasPDF hns hnt hu
have : IsProbabilityMeasure ℙ := isProbabilityMeasure hns hnt hu
apply (eq_of_map_eq_withDensity _ _).mp
· rw [hu, withDensity_indicator hms, withDensity_smul _ measurable_one, withDensity_one, ProbabilityTheory.cond]
· exact (measurable_one.aemeasurable.const_smul (μ s)⁻¹).indicator hms
