Real functions Differentiation Theorem
Mean value theorem
Builds on Rolle's theorem
Statement
Let and let be continuous on and differentiable on . Then there is with
Remarks
Apply Rolle's theorem to , which has .
It turns bounds on into bounds on . It gives zero derivative implies constant and the monotonicity tests.
Mathlib states it as exists_deriv_eq_slope.
History
Augustin-Louis Cauchy stated and proved the theorem in its modern form in 1823.
Reading path
To understand this page from the ground up, read these 22 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
- Mean value theorem statement
Where this leads
103 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
- 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
- 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
- Failure of Aizerman's conjecture
- Frullani integral
- Gauss's test
- Log-convexity of the gamma function
- Differentiation operator as inverse of integration
- Logarithmically convex function
- Cauchy formula for repeated integration
- Borel's lemma
- Viète's formula
- Cantor function
- Bohr–Mollerup theorem
- Volterra's function
- An infinite product converges iff its series of logarithms converges
- Trigonometric integrals
- Basel problem via Fourier series
- Abel's summation formula
- Barnes G-function
- Chudnovsky algorithm
Further reading
About this page
| Tag | 0BARQY52N5 |
|---|---|
| URI | m2://0BARQY52N5 |
| Aliases | lagrange-mean-value-theorem |
| Kind | statement, theorem |
| Writing | W1 stated |
| MSC | 26A24 |
| Status | This copy of the site has no build data. Run m2 status 0BARQY52N5. |
| Uses | Rolle's theorem |
| 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.
What links here
Used by
- A function with zero derivative is constant
- A differentiable function is convex iff its derivative is increasing
- Taylor's theorem with the Cauchy remainder
- A function with nonnegative derivative is increasing
- Cauchy mean value theorem
- A function with positive derivative is strictly increasing
- Uniform convergence of derivatives allows term-by-term differentiation
- A function with bounded derivative is Lipschitz
- Second fundamental theorem of calculus
- Difference quotient
- Failure of Aizerman's conjecture