Integrals involving the Gamma function

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

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)

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)

theorem integral_exp_neg_rpow {p : ℝ} (hp : 0 < p) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-x ^ p) = Real.Gamma (1 / p + 1)

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)

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)

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)

theorem Complex.integral_exp_neg_rpow {p : ℝ} (hp : 1 ≤ p) : ∫ (x : ℂ), Real.exp (-‖x‖ ^ p) = Real.pi * Real.Gamma (2 / p + 1)

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)