English
The integral of the beta pdf over ℝ equals the integral over (0,1) of ENNReal.ofReal of the same density expression.
Русский
Интеграл плотности бета-распределения по всей действительной оси равен интегралу по отрезку (0,1) от той же функции плотности.
LaTeX
$$$\int^- x\, \betaPDF(\alpha,\beta,x) \,dx = \int^- x\in Ioo(0,1)\, \mathrm{ENNReal}.ofReal\left(\frac{1}{\beta(\alpha,\beta)} x^{\alpha-1}(1-x)^{\beta-1}\right) \,dx$$$
Lean4
theorem lintegral_betaPDF {α β : ℝ} :
∫⁻ x, betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) := by
rw [← lintegral_add_compl _ measurableSet_Iic,
setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx), zero_add, compl_Iic, ←
lintegral_add_compl _ measurableSet_Ici,
setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx), zero_add, compl_Ici,
Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
setLIntegral_congr_fun measurableSet_Ioo (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
