# Integrals involving the Gamma function #

In this file, we collect several integrals over `ℝ` or `ℂ` that evaluate in terms of the `Real.Gamma` function.

source
theorem integral_rpow_mul_exp_neg_rpow {p q : ℝ} (hp : 0 < p) (hq : -1 < q) :
∫ (x : ℝ) in Set.Ioi 0, x ^ q * Real.exp (-x ^ p) = 1 / p * Real.Gamma ((q + 1) / p)
source
theorem integral_rpow_mul_exp_neg_mul_rpow {p q b : ℝ} (hp : 0 < p) (hq : -1 < q) (hb : 0 < b) :
∫ (x : ℝ) in Set.Ioi 0, x ^ q * Real.exp (-b * x ^ p) = b ^ (-(q + 1) / p) * (1 / p) * Real.Gamma ((q + 1) / p)
source
theorem integral_exp_neg_rpow {p : ℝ} (hp : 0 < p) :
∫ (x : ℝ) in Set.Ioi 0, Real.exp (-x ^ p) = Real.Gamma (1 / p + 1)
source
theorem integral_exp_neg_mul_rpow {p b : ℝ} (hp : 0 < p) (hb : 0 < b) :
∫ (x : ℝ) in Set.Ioi 0, Real.exp (-b * x ^ p) = b ^ (-1 / p) * Real.Gamma (1 / p + 1)
source
theorem Complex.integral_rpow_mul_exp_neg_rpow {p q : ℝ} (hp : 1 ≤ p) (hq : -2 < q) :
∫ (x : ℂ), ‖x‖ ^ q * Real.exp (-‖x‖ ^ p) = 2 * Real.pi / p * Real.Gamma ((q + 2) / p)
source
theorem Complex.integral_rpow_mul_exp_neg_mul_rpow {p q b : ℝ} (hp : 1 ≤ p) (hq : -2 < q) (hb : 0 < b) :
∫ (x : ℂ), ‖x‖ ^ q * Real.exp (-b * ‖x‖ ^ p) = 2 * Real.pi / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
source
theorem Complex.integral_exp_neg_rpow {p : ℝ} (hp : 1 ≤ p) :
∫ (x : ℂ), Real.exp (-‖x‖ ^ p) = Real.pi * Real.Gamma (2 / p + 1)
source
theorem Complex.integral_exp_neg_mul_rpow {p b : ℝ} (hp : 1 ≤ p) (hb : 0 < b) :
∫ (x : ℂ), Real.exp (-b * ‖x‖ ^ p) = Real.pi * b ^ (-2 / p) * Real.Gamma (2 / p + 1)