English
If X is uniform on s with Lebesgue volume, then E[X] = (volume s)⁻¹ ∫_s x.
Русский
Если X равномерна на s относительно объёма Лебега, то математическое ожидание X равно (vol s)⁻¹∫_s x.
LaTeX
$$$\\mathbb{E}[X] = (\\operatorname{vol} s)^{-1} \\int_{s} x \\, dx$$$
Lean4
/-- A real uniform random variable `X` with support `s` has expectation
`(λ s)⁻¹ * ∫ x in s, x ∂λ` where `λ` is the Lebesgue measure. -/
theorem integral_eq (huX : IsUniform X s ℙ) : ∫ x, X x ∂ℙ = (volume s)⁻¹.toReal * ∫ x in s, x :=
by
rw [← smul_eq_mul, ← integral_smul_measure]
dsimp only [IsUniform, ProbabilityTheory.cond] at huX
rw [← huX]
by_cases hX : AEMeasurable X ℙ
· exact (integral_map hX aestronglyMeasurable_id).symm
· rw [map_of_not_aemeasurable hX, integral_zero_measure, integral_non_aestronglyMeasurable]
rwa [aestronglyMeasurable_iff_aemeasurable]
