Math 2.0

Special functions Proposition

1 + x is at most exp x

Builds on The exponential function is convexA differentiable function is convex iff its derivative is increasing

Statement

For every real xx, 1+x≤ex,1 + x \le e^x, with equality if and only if x=0x = 0.

Remarks

The line y=1+xy = 1 + x is the tangent to the graph of exe^x at 00. The graph of a convex function lies above its tangent lines, by the derivative criterion. For x≥0x \ge 0 the claim also follows from the series, since the other terms are nonnegative. Taking logarithms gives ln⁡y≤y−1\ln y \le y - 1 for y>0y > 0. Mathlib states the inequality as Real.add_one_le_exp.

Reading path

To understand this page from the ground up, read these 55 pages in order. The foundations come first.

  1. Convex function definition
  2. Limit point of a set definition
  3. Local maximum definition
  4. Sequence definition
  5. Slopes of a convex function are increasing statement
  6. Limit of a function definition
  7. Local minimum definition
  8. Real sequence definition
  9. Subsequence definition
  10. Continuity at a point definition
  11. Derivative definition
  12. Bounded sequence definition
  13. Geometric sequence definition
  14. Limit of a sequence definition
  15. Monotone sequence definition
  16. Series definition
  17. Continuous function definition
  18. Differentiable function definition
  19. Fermat's theorem on stationary points statement
  20. Sum of a finite geometric series statement
  21. Monotone convergence theorem for sequences statement
  22. Convergent sequence definition
  23. Squeeze theorem statement
  24. Every sequence has a monotone subsequence statement
  25. Cauchy product definition
  26. Partial sum definition
  27. Power series definition
  28. Derivative function definition
  29. The sequence r^n tends to zero for |r| < 1 example
  30. Bolzano–Weierstrass theorem statement
  31. Radius of convergence definition
  32. Convergent series definition
  33. Higher derivative definition
  34. Boundedness theorem statement
  35. Absolute convergence definition
  36. A series of nonnegative terms converges iff its partial sums are bounded statement
  37. Sum of a series definition
  38. Second derivative definition
  39. Extreme value theorem statement
  40. Geometric series example
  41. Comparison test statement
  42. Cauchy product of absolutely convergent series statement
  43. Rolle's theorem statement
  44. Ratio test statement
  45. Mean value theorem statement
  46. Ratio formula for the radius of convergence statement
  47. A differentiable function is convex iff its derivative is increasing statement
  48. A function with nonnegative derivative is increasing statement
  49. The exponential series has infinite radius of convergence statement
  50. A function with nonnegative second derivative is convex statement
  51. Exponential function definition
  52. Exponential of a sum statement
  53. The exponential function is its own derivative statement
  54. The exponential function is convex statement
  55. 1 + x is at most exp x statement

Where this leads

1 page builds on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Exponential_function, Properties
About this page
Tag012C7GFF20
URIm2://012C7GFF20
Kindstatement, proposition
WritingW0 stub
MSC33B10, 26D15
StatusThis copy of the site has no build data. Run m2 status 012C7GFF20.
UsesThe exponential function is convex, A differentiable function is convex iff its derivative is increasing

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • an inventory row: the row of the inventory that the node accounts for (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Used by