English
For a > 0 and r > 0, the lintegral of gammaPDF over all real numbers equals 1.
Русский
Для a > 0 и r > 0 линегральный интеграл гамма-плотности по всей реальности равен 1.
LaTeX
$$$\int^{-} x\,\gammaPDF(a,r,x)\;dx = 1$$$
Lean4
/-- The pdf of the gamma distribution integrates to 1 -/
@[simp]
theorem lintegral_gammaPDF_eq_one {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : ∫⁻ x, gammaPDF a r x = 1 :=
by
have leftSide : ∫⁻ x in Iio 0, gammaPDF a r x = 0 := by
rw [setLIntegral_congr_fun measurableSet_Iio (fun x (hx : x < 0) ↦ gammaPDF_of_neg hx), lintegral_zero]
have rightSide :
∫⁻ x in Ici 0, gammaPDF a r x = ∫⁻ x in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * exp (-(r * x))) :=
setLIntegral_congr_fun measurableSet_Ici (fun _ ↦ gammaPDF_of_nonneg)
rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici, leftSide, rightSide, add_zero,
← integral_eq_lintegral_of_nonneg_ae]
· simp_rw [integral_Ici_eq_integral_Ioi, mul_assoc]
rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div, ← mul_assoc, mul_div_assoc,
div_self (Gamma_pos_of_pos ha).ne', mul_one, div_rpow zero_le_one hr.le, one_rpow, mul_one_div,
div_self (rpow_pos_of_pos hr _).ne']
· rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]
exact ae_of_all _ (fun x (hx : 0 ≤ x) ↦ by positivity)
· apply (measurable_gammaPDFReal a r).aestronglyMeasurable.congr
refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : 0 ≤ x) ↦ ?_
simp_rw [gammaPDFReal, eq_true_intro hx, ite_true]
