Theorems · Definition · real analysis
Real.mulExpNegMulSq
ℝ → ℝ → ℝ
Mapping fun ε x => x * Real.exp (- (ε * x * x)). By composition, it can be used to transform
functions into bounded functions.
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by29
Results whose statement or proof uses this declaration.
- Continuous.mulExpNegMulSqstatement · cited by 3
- Real.abs_mulExpNegMulSq_lestatement and proof · cited by 2
- Real.mulExpNegMulSq_one_le_onestatement · cited by 2
- dist_integral_mulExpNegMulSq_comp_lestatement and proof · cited by 1
- Real.nnnorm_deriv_mulExpNegMulSq_le_onestatement and proof · cited by 1
- Real.continuous_mulExpNegMulSqstatement · cited by 1
- Real.norm_deriv_mulExpNegMulSq_le_onestatement and proof · cited by 1
- Real.hasDerivAt_mulExpNegMulSqstatement and proof · cited by 1
- Real.dist_mulExpNegMulSq_le_diststatement and proof · cited by 1
- Real.dist_mulExpNegMulSq_le_two_mul_sqrtstatement and proof · cited by 1
- Real.abs_mulExpNegMulSq_comp_le_normstatement · cited by 1