Math 2.0

statement theorem

Fermat's theorem on stationary points

Statement

Let II be an open interval, let f ⁣:I→Rf \colon I \to \mathbb{R}, and let a∈Ia \in I. Assume that ff has a local maximum or a local minimum at aa, and that ff is differentiable at aa. Then f′(a)=0f'(a) = 0.

Remarks

At a local maximum, the difference quotient (f(a+h)−f(a))/h(f(a + h) - f(a))/h is ≤0\le 0 for small h>0h > 0 and ≥0\ge 0 for small h<0h < 0. So the limit is both ≤0\le 0 and ≥0\ge 0. The point must be interior. On [0,1][0, 1], the function xx has a maximum at 11, where its derivative is 11. Mathlib states it as IsLocalExtr.deriv_eq_zero.

Explanations

L1 human

At the top of a smooth hill, the tangent line is horizontal. If the slope were positive or negative, moving a little would give a higher value.

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 6 nodes in this order. The foundations come first, and the list ends with this node.

Each node uses the nodes above it. The colour of the bar on a box shows the evidence level, and the box also gives it as text. The list below has the same nodes.
  • no evidence level
  1. Limit point of a set definition
  2. Local maximum definition
  3. Limit of a function definition
  4. Local minimum definition
  5. Derivative definition
  6. Fermat's theorem on stationary points statement

What depends on this

78 nodes use this node, directly or through other nodes.

Sources

  1. Web https://en.wikipedia.org/wiki/Interior_extremum_theorem, Statement