Theorems · Theorem · real analysis
Real.nnnorm_deriv_mulExpNegMulSq_le_one
∀ {ε : ℝ}, 0 < ε → ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1- Cited by
- 1 results in Mathlib
- Foundations
- Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- NNRealstatement · cited by 4,310
- NNReal.toRealproof · cited by 1,260
- NNNorm.nnnormstatement · cited by 952
- derivstatement and proof · cited by 676
- NNReal.coe_le_coeproof · cited by 73
- coe_nnnormproof · cited by 33
- Real.mulExpNegMulSqstatement and proof · cited by 29
- Real.norm_deriv_mulExpNegMulSq_le_oneproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Real.lipschitzWith_one_mulExpNegMulSqproof · cited by 1