English
If X is uniform on a measurable set s with a nondegenerate finite measure, then X has a density with respect to μ and ℙ.
Русский
Если X равномерна на измеримом множестве s с ненулем и конечной мерой, то X имеет плотность относительно μ и ℙ.
LaTeX
$$$\\text{HasPDF}(X, \\mathbb{P}, \\mu)$$$
Lean4
theorem hasPDF {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) (hu : IsUniform X s ℙ μ) : HasPDF X ℙ μ :=
by
let t := toMeasurable μ s
apply
hasPDF_of_map_eq_withDensity (hu.aemeasurable hns hnt) (t.indicator ((μ t)⁻¹ • 1)) <|
(measurable_one.aemeasurable.const_smul (μ t)⁻¹).indicator (measurableSet_toMeasurable μ s)
rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one, withDensity_one,
restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]
