Theorems · Theorem · real analysis
convexOn_exp
ConvexOn ℝ Set.univ Real.exp
Real.exp is convex on the whole real line.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Set.univstatement · cited by 3,945
- Real.expstatement · cited by 871
- ConvexOnstatement · cited by 232
- StrictConvexOn.convexOnproof · cited by 10
- strictConvexOn_expproof · cited by 2
Cited by5
Results whose statement or proof uses this declaration.
- Real.geom_mean_le_arith_mean_weightedproof · cited by 5
- Real.convexOn_Gammaproof · cited by 2
- Polynomial.mahlerMeasure_le_sqrt_sum_sq_norm_coeffproof · cited by 1
- Real.exp_mul_le_cosh_add_mul_sinhproof · cited by 0
- convexOn_rpow_leftproof · cited by 0