Theorems · Theorem · real analysis
sum_Ico_pow_mul_exp_neg_le
∀ {k M : ℕ} {c : ℝ},
0 < c → ∑ i ∈ Finset.Ico 0 M, ↑i ^ k * Real.exp (-(c * ↑i)) ≤ Real.exp c * ↑k.factorial / c ^ (k + 1)- Defined in
- Mathlib.Analysis.SumIntegralExpDecay
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 289 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites25
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Finset.sumstatement · cited by 5,195
- mul_oneproof · cited by 3,885
- mul_commproof · cited by 2,262
- Set.Iccproof · cited by 1,702
- MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
- le_of_ltproof · cited by 1,175
- sub_eq_add_negproof · cited by 1,023
- Real.expstatement and proof · cited by 871
- Nat.factorialstatement and proof · cited by 616
- intervalIntegralproof · cited by 546
- Finset.Icostatement · cited by 450
Cited by1
Results whose statement or proof uses this declaration.
- sum_Iic_pow_mul_exp_neg_leproof · cited by 1