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)