Real functions Differentiation Theorem
Rolle's theorem
Builds on Extreme value theoremFermat's theorem on stationary points
Statement
Let and let be continuous on and differentiable on , with . Then there is with .
Remarks
By the extreme value theorem, has a maximum and a minimum on . If both occur at the endpoints, is constant. Otherwise one occurs at an interior point , and Fermat's theorem gives .
Differentiability inside the interval is needed. The function on has no point with derivative .
Mathlib states it as exists_deriv_eq_zero.
History
Michel Rolle proved a version for polynomials in 1691. Cauchy gave a proof of the general theorem in 1823.
Reading path
To understand this page from the ground up, read these 21 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Limit point of a set definition
- Local maximum definition
- Sequence definition
- 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
Where this leads
112 pages build on this one.
- Power series are differentiable inside the radius of convergence
- A function with zero derivative is constant
- Natural logarithm
- A differentiable function is convex iff its derivative is increasing
- Taylor's theorem with the Cauchy remainder
- Euler–Mascheroni constant
- The logarithm grows slower than any power
- Derivative of sine
- 1 + x is at most exp x
- Reduction formula
- First derivative test
- cos pi = -1
- sin x / x tends to 1
- A function with nonnegative derivative is increasing
- Inverse trigonometric functions
- Cauchy mean value theorem
- Leibniz formula for pi
- Integral of exp(-x) over the half line
- Pythagorean trigonometric identity
- log x is at most x - 1
- Inverse hyperbolic functions
- Integral of cosine
- Derivative of arctangent
- Harmonic numbers grow like log n
- Integral of the exponential function
- A function with positive derivative is strictly increasing
- Derivative of the logarithm
- Integration by parts
- Arcsine
- Mean value theorem
- pi
- Uniform convergence of derivatives allows term-by-term differentiation
- Integration by substitution
- The exponential function is convex
- Basel problem
- Trigonometric substitution
- The gamma function extends the factorial
- Second derivative test
- Derivative of arcsine
- Area under a curve
- Integral of sine
- Dirichlet integral
- Taylor's theorem with the Lagrange remainder
- Logarithm of a quotient
- L'Hôpital's rule
- Integral of 1/x
- Logarithm of a product
- Stirling's formula
- The exponential function is strictly increasing
- Derivative of x^a
- Fundamental theorem of calculus
- Sine is 2π-periodic
- A function with bounded derivative is Lipschitz
- Integral of a power
- Irrationality of pi
- pi is greater than 3
- Arccosine
- Logarithm is the inverse of the exponential
- Power-reduction formula for cosine
- Derivative of tangent
- Power series of arctangent
- Term-by-term differentiation
- Real exponentiation
- Derivative of cosine
- Logarithm of a power
- Improper integral of x^p on an unbounded interval
- Tangent half-angle substitution
- Integration by partial fractions
- Taylor's theorem with the integral remainder
- Wallis product
- Second fundamental theorem of calculus
- Mercator series
- A function with nonnegative second derivative is convex
- The logarithm is strictly concave
- Arnold tongue
- Lebesgue's theorem on differentiability of monotone functions
- Minimal curvature property of natural cubic splines
- Stein's unbiased risk estimate
- Weierstrass product for the gamma function
- Stein's lemma
- Bertrand's test
- Mertens' theorems
- Peano kernel theorem
- Stein's example
- Reduction of an initial value problem to a Volterra equation
- Ramanujan's series for 1/pi
- Difference quotient
- Quadratic convergence of Newton's method
- Failure of Aizerman's conjecture
- Frullani integral
- Gauss's test
- Log-convexity of the gamma function
- Mean value theorem for divided differences
- Differentiation operator as inverse of integration
- Logarithmically convex function
- Cauchy formula for repeated integration
- Interpolation error formula
- Borel's lemma
- Viète's formula
- Cantor function
- Error bound for the trapezoidal rule
- Bohr–Mollerup theorem
- Volterra's function
- An infinite product converges iff its series of logarithms converges
- Quintic equation
- Descartes' rule of signs
- Trigonometric integrals
- Basel problem via Fourier series
- Abel's summation formula
- Barnes G-function
- Chudnovsky algorithm
- Runge's phenomenon
Further reading
About this page
| Tag | 0194DY35BG |
|---|---|
| URI | m2://0194DY35BG |
| Kind | statement, theorem |
| Writing | W1 stated |
| MSC | 26A24 |
| Status | This copy of the site has no build data. Run m2 status 0194DY35BG. |
| Uses | Extreme value theorem, Fermat's theorem on stationary points |
| Same as |
Markdown · JSON · Edit on GitHub
What this page needs for W2
- edge about out: the concepts that the statement is about (0 of 1)
- edge proves in: at least one proof node (0 of 1)
- edge instance_of or illustrates in: one example that shows the statement at work (0 of 1)
- explanation L2 (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.