English
If α > 0 and β > 0, then the lintegral of betaPDF α β over ℝ equals 1.
Русский
Если α > 0 и β > 0, то линегральная норма betaPDF α β по ℝ равна 1.
LaTeX
$$$\text{lintegral}_{\mathbb{R}}\, \betaPDF(\alpha,\beta, x)\,dx = 1\quad(\alpha>0,\beta>0)$$$
Lean4
/-- The pdf of the beta distribution integrates to 1. -/
@[simp]
theorem lintegral_betaPDF_eq_one {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : ∫⁻ x, betaPDF α β x = 1 :=
by
rw [lintegral_betaPDF, ← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae]
· simp_rw [mul_assoc, integral_const_mul]
field_simp
rw [div_eq_one_iff_eq (ne_of_gt (beta_pos hα hβ)), beta_eq_betaIntegralReal α β hα hβ, betaIntegral,
intervalIntegral.integral_of_le (by norm_num), ← integral_Ioc_eq_integral_Ioo, ← RCLike.re_to_complex, ←
integral_re]
· refine setIntegral_congr_fun measurableSet_Ioc fun x ⟨hx1, hx₂⟩ ↦ ?_
norm_cast
rw [← Complex.ofReal_cpow, ← Complex.ofReal_cpow, RCLike.re_to_complex, Complex.re_mul_ofReal, Complex.ofReal_re]
all_goals linarith
convert betaIntegral_convergent (u := α) (v := β) (by simpa) (by simpa)
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by simp), IntegrableOn]
· refine ae_restrict_of_forall_mem measurableSet_Ioo (fun x hx ↦ ?_)
convert betaPDFReal_pos hx.1 hx.2 hα hβ |>.le using 1
rw [betaPDFReal, if_pos ⟨hx.1, hx.2⟩]
· exact Measurable.aestronglyMeasurable (by fun_prop)
