theorem
Verification.gamma_integral_rpow
{a b k : ℝ}
(ha : 0 < a)
(hb : 0 < b)
(hak : 0 < a + k)
:
MeasureTheory.Integrable (fun (t : ℝ) => t ^ k) (ProbabilityTheory.gammaMeasure a b) ∧ ∫ (t : ℝ), t ^ k ∂ProbabilityTheory.gammaMeasure a b = b ^ a / Real.Gamma a * Real.Gamma (a + k) / b ^ (a + k)
theorem
Verification.gammaPrecision_first_moment
{a : ℝ}
(ha : 0 < a)
:
MeasureTheory.Integrable (fun (t : ℝ) => t) (ProbabilityTheory.gammaMeasure a a) ∧ ∫ (t : ℝ), t ∂ProbabilityTheory.gammaMeasure a a = 1
theorem
Verification.gammaPrecision_second_moment
{a : ℝ}
(ha : 0 < a)
:
MeasureTheory.Integrable (fun (t : ℝ) => t ^ 2) (ProbabilityTheory.gammaMeasure a a) ∧ ∫ (t : ℝ), t ^ 2 ∂ProbabilityTheory.gammaMeasure a a = 1 + a⁻¹
theorem
Verification.gammaPrecision_centered_second_moment
{a : ℝ}
(ha : 0 < a)
:
MeasureTheory.Integrable (fun (t : ℝ) => (t - 1) ^ 2) (ProbabilityTheory.gammaMeasure a a) ∧ ∫ (t : ℝ), (t - 1) ^ 2 ∂ProbabilityTheory.gammaMeasure a a = a⁻¹