Math 2.0

statement proposition

log x is at most x - 1

Statement

For every real x>0x > 0, ln⁡x≤x−1,\ln x \le x - 1, with equality if and only if x=1x = 1.

Remarks

Put ln⁡x\ln x into the inequality 1+y≤ey1 + y \le e^y. Then 1+ln⁡x≤eln⁡x=x1 + \ln x \le e^{\ln x} = x. The line y=x−1y = x - 1 is the tangent to the graph of ln⁡\ln at x=1x = 1. Replacing xx by 1/x1/x gives ln⁡x≥1−1/x\ln x \ge 1 - 1/x. Mathlib states the main claim as Real.log_le_sub_one_of_pos.

Explanations

L1 human

The graph of ln⁡\ln lies below its tangent line at x=1x = 1. This follows from the concavity of the logarithm.

What this node 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 node is. They do not measure its truth.

What this needs

To read this node, read these 66 nodes in this order. The foundations come first, and the list ends with this node.

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

Sources

  1. Web https://en.wikipedia.org/wiki/Natural_logarithm, Definition and properties

What links here

No node links to this node yet.