statement theorem
A differentiable function is convex iff its derivative is increasing
Statement
Let be an open interval and let be differentiable. Then is convex if and only if is increasing on .
Remarks
If is convex, the slope inequalities give for .
If is increasing, the mean value theorem on and gives the slope inequalities.
Then the graph lies above each tangent line: .
Mathlib states the converse direction as MonotoneOn.convexOn_of_deriv.
Explanations
L1 human
A differentiable function is convex when its slope keeps growing. The graph then turns to the left as we move along it to the right.
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 25 nodes in this order. The foundations come first, and the list ends with this node.
- no evidence level
- Convex function definition
- Limit point of a set definition
- Local maximum definition
- Sequence definition
- Slopes of a convex function are increasing statement
- Limit of a function definition
- Local minimum definition
- Real sequence definition
- Subsequence definition
- Continuity at a point definition
- Derivative definition
- Bounded sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Continuous function definition
- Fermat's theorem on stationary points statement
- Convergent sequence definition
- Monotone convergence theorem for sequences statement
- Every sequence has a monotone subsequence statement
- Bolzano–Weierstrass theorem statement
- Boundedness theorem statement
- Extreme value theorem statement
- Rolle's theorem statement
- Mean value theorem statement
- A differentiable function is convex iff its derivative is increasing statement
What depends on this
4 nodes use this node, directly or through other nodes.
- 1 + x is at most exp x 012C7GFF20
- log x is at most x - 1 04CBRA4JRK
- The exponential function is convex 0D7GRZ2ADX
- A function with nonnegative second derivative is convex 0Z41C17TGP
Sources
- Web https://en.wikipedia.org/wiki/Convex_function, Functions of one variable
What links here
Used by
- 1 + x is at most exp x 012C7GFF20
- A function with nonnegative second derivative is convex 0Z41C17TGP