Theorems · Theorem · special functions
Real.summable_pow_mul_exp_neg_nat_mul
∀ (k : ℕ) {r : ℝ}, 0 < r → Summable fun n => ↑n ^ k * Real.exp (-r * ↑n)- Defined in
- Mathlib.Analysis.SpecialFunctions.Exp
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- mul_commproof · cited by 2,262
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- Real.expstatement and proof · cited by 871
- Summablestatement and proof · cited by 778
- Real.norm_of_nonnegproof · cited by 135
- neg_lt_zeroproof · cited by 36
- Real.exp_nonnegproof · cited by 21
- Real.exp_lt_one_iffproof · cited by 7
- Real.exp_nat_mulproof · cited by 6
- summable_pow_mul_geometric_of_norm_lt_oneproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- summable_pow_mul_jacobiTheta₂_term_boundproof · cited by 6