Theorems · Theorem · real analysis
tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero
∀ (s b : ℝ), 0 < b → Filter.Tendsto (fun x => x ^ s * Real.exp (-b * x)) Filter.atTop (nhds 0)
The function x ^ s * exp (-b * x) tends to 0 at +∞, for any real s and b > 0.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- nhdsstatement · cited by 5,554
- Filter.Tendstostatement · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- Filter.univ_mem'proof · cited by 1,672
- Real.expstatement and proof · cited by 871
- div_eq_mul_invproof · cited by 715
- neg_mulproof · cited by 654
- Filter.Tendsto.congr'proof · cited by 154
- inv_divproof · cited by 92
- Real.exp_negproof · cited by 28
- Filter.Tendsto.inv_tendsto_atTopproof · cited by 21
Cited by4
Results whose statement or proof uses this declaration.
- isLittleO_rpow_exp_pos_mul_atTopproof · cited by 2
- isLittleO_exp_mul_rpow_of_ltproof · cited by 1
- Real.tendsto_integral_gaussian_smul'proof · cited by 1
- Complex.GammaIntegral_add_oneproof · cited by 0