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 * (-x ^ p).exp = 1 / p * ((q + 1) / p).Gamma

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 * (-b * x ^ p).exp = b ^ (-(q + 1) / p) * (1 / p) * ((q + 1) / p).Gamma

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

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

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

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

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

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