Theorems · Theorem · real analysis
Real.abs_mulExpNegMulSq_le
∀ {ε : ℝ}, 0 < ε → ∀ {x : ℝ}, |ε.mulExpNegMulSq x| ≤ (√ε)⁻¹For fixed ε > 0, the mapping x ↦ mulExpNegMulSq ε x is bounded by (√ε)⁻¹.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- absstatement and proof · cited by 1,814
- le_of_ltproof · cited by 1,175
- Real.sqrtstatement and proof · cited by 545
- inv_pos_of_posproof · cited by 123
- abs_of_posproof · cited by 114
- abs_mulproof · cited by 98
- Real.sqrt_pos_of_posproof · cited by 50
- mul_le_of_le_one_rightproof · cited by 29
- Real.mulExpNegMulSqstatement and proof · cited by 29
- Real.abs_mulExpNegMulSq_one_le_oneproof · cited by 1
- Real.mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_oneproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- abs_integral_sub_setIntegral_mulExpNegMulSq_comp_ltproof · cited by 1
- Real.dist_mulExpNegMulSq_le_two_mul_sqrtproof · cited by 1