theorem
Verification.gammaPDF_power_exp
{a b k d x : ℝ}
(ha : 0 < a)
(hb : 0 < b)
(hak : 0 < a + k)
(hbd : 0 < b + d)
(hx : 0 < x)
:
ProbabilityTheory.gammaPDF a b x * ENNReal.ofReal (x ^ k * Real.exp (-(d * x))) = ENNReal.ofReal (b ^ a / Real.Gamma a * Real.Gamma (a + k) / (b + d) ^ (a + k)) * ProbabilityTheory.gammaPDF (a + k) (b + d) x
theorem
Verification.lintegral_power_exp_gammaMeasure
{a b k d : ℝ}
(ha : 0 < a)
(hb : 0 < b)
(hak : 0 < a + k)
(hbd : 0 < b + d)
:
∫⁻ (x : ℝ), ENNReal.ofReal (x ^ k * Real.exp (-(d * x))) ∂ProbabilityTheory.gammaMeasure a b = ENNReal.ofReal (b ^ a / Real.Gamma a * Real.Gamma (a + k) / (b + d) ^ (a + k))