Bounds for sums and integrals of x ^ k * exp (-c * x)

We bound the integral and sums of x ^ k * exp (-c * x) by k ! / c ^ (k + 1), using the Gamma function.

theorem intervalIntegral_pow_mul_exp_neg_le {k : ℕ} {M c : ℝ} (hM : 0 ≤ M) (hc : 0 < c) : ∫ (x : ℝ) in 0..M, x ^ k * Real.exp (-(c * x)) ≤ ↑k.factorial / c ^ (k + 1)

theorem sum_Ico_pow_mul_exp_neg_le {k M : ℕ} {c : ℝ} (hc : 0 < c) : ∑ i ∈ Finset.Ico 0 M, ↑i ^ k * Real.exp (-(c * ↑i)) ≤ Real.exp c * ↑k.factorial / c ^ (k + 1)

theorem sum_Iic_pow_mul_exp_neg_le {k M : ℕ} {c : ℝ} (hc : 0 < c) : ∑ i ∈ Finset.Iic M, ↑i ^ k * Real.exp (-(c * ↑i)) ≤ Real.exp c * ↑k.factorial / c ^ (k + 1)

theorem sum_Iic_pow_mul_two_pow_neg_le {k M : ℕ} {c : ℝ} (hc : 0 < c) : ∑ i ∈ Finset.Iic M, ↑i ^ k * 2 ^ (-(c * ↑i)) ≤ 2 ^ c * ↑k.factorial / (Real.log 2 * c) ^ (k + 1)