English
Let X be a map Ω → E and s ⊂ E with μ(s) ≠ 0 and μ(s) ≠ ∞. If X is uniform on s with respect to ℙ and μ (i.e., IsUniform X s ℙ μ), then X is almost everywhere measurable with respect to ℙ and μ.
Русский
Пусть X: Ω → E и s ⊂ E удовлетворяют μ(s) ≠ 0 и μ(s) ≠ ∞. Если X равномерно распределён на s относительно ℙ и μ (IsUniform X s ℙ μ), то X есть а.е. измеримо по отношению к ℙ и μ.
LaTeX
$$$\\text{AEMeasurable}(X,\\mathbb{P})$$$
Lean4
theorem aemeasurable {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) (hu : IsUniform X s ℙ μ) :
AEMeasurable X ℙ := by
dsimp [IsUniform, ProbabilityTheory.cond] at hu
by_contra h
rw [map_of_not_aemeasurable h] at hu
apply zero_ne_one' ℝ≥0∞
calc
0 = (0 : Measure E) Set.univ := rfl
_ = _ := by
rw [hu, smul_apply, restrict_apply MeasurableSet.univ, Set.univ_inter, smul_eq_mul,
ENNReal.inv_mul_cancel hns hnt]
