English
If s is compact, the product x·pdf(x) is integrable with respect to volume for the real-valued X.
Русский
Если множество s компактно, то интеграл от x·pdf(x) по объёму конечен для вещественного X.
LaTeX
$$$\\int x\\, pdf(X,\\mathbb{P}, volume)(x)\\, dx$ существует и конечен; более precisely, integrable.$$
Lean4
theorem mul_pdf_integrable (hcs : IsCompact s) (huX : IsUniform X s ℙ) :
Integrable fun x : ℝ => x * (pdf X ℙ volume x).toReal :=
by
by_cases hnt : volume s = 0 ∨ volume s = ∞
· have I : Integrable (fun x ↦ x * ENNReal.toReal (0)) := by simp
apply I.congr
filter_upwards [pdf_eq_zero_of_measure_eq_zero_or_top huX hnt] with x hx
simp [hx]
simp only [not_or] at hnt
have : IsProbabilityMeasure ℙ := isProbabilityMeasure hnt.1 hnt.2 huX
constructor
· exact aestronglyMeasurable_id.mul (measurable_pdf X ℙ).aemeasurable.ennreal_toReal.aestronglyMeasurable
refine hasFiniteIntegral_mul (pdf_eq hcs.measurableSet huX) ?_
set ind := (volume s)⁻¹ • (1 : ℝ → ℝ≥0∞)
have : ∀ x, ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x := fun x =>
(s.indicator_mul_right (fun x => ↑‖x‖₊) ind).symm
simp only [ind, this, lintegral_indicator hcs.measurableSet, mul_one, Algebra.id.smul_eq_mul, Pi.one_apply,
Pi.smul_apply]
rw [lintegral_mul_const _ measurable_enorm]
exact
ENNReal.mul_ne_top (setLIntegral_lt_top_of_isCompact hnt.2 hcs continuous_nnnorm).ne
(ENNReal.inv_lt_top.2 (pos_iff_ne_zero.mpr hnt.1)).ne
