How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with
Statement
Let with and let be continuous on (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point, Intervals of : the nine order-convex forms, nondegeneracy, and length) and differentiable at every point of as a function on (The derivative of at a point that is a limit point of , and differentiability on a set). Then there is with
Equivalently, since , there is at which : the derivative somewhere inside equals the average rate of change across the whole interval.
Continuity on the closed interval cannot be dropped. Differentiability at every point of alone does not suffice: a function on , differentiable at every point of with derivative constantly , for which no works, is exhibited later on this page as a false statement, and the companion page works the same witness out in full.
Statement references
Facts & Assumptions
Given: Reals and a function continuous on and differentiable at every point of .
Cauchy's mean value theorem (Cauchy's mean value theorem: for continuous on with and differentiable on there is with ; no hypothesis on is needed in this product form): for continuous on and differentiable at every point of there is with .
The identity is continuous at every point of any (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, claim 5).
The identity on is differentiable at every with : with the set is order-convex with at least two elements, so every one of its points is a limit point of it (The derivative of at a point that is a limit point of , and differentiability on a set, Intervals of : the nine order-convex forms, nondegeneracy, and length); and the difference quotient of at is for every with , a constant function, whose limit at is (The - limit of at a limit point of , The derivative of at a point that is a limit point of , and differentiability on a set).
Proof
Define by .
is continuous on by [L2]; it is differentiable at every with by [L3]; and .
By step 2.1 the pair satisfies every hypothesis of [L1], so there is with . Substituting and gives .
Remarks
-
The geometric reading, and what it is not. The conclusion says that some tangent line is parallel to the chord from to . It does not say which one, it does not say there is only one, and it says nothing at all about between the endpoints beyond the hypotheses. Every use of the theorem on this page is a use of the equation, never of the picture.
-
Why this is a corollary and not the primitive statement. Cauchy's mean value theorem: for continuous on with and differentiable on there is with ; no hypothesis on is needed in this product form is proved from Rolle's theorem: if , is continuous on , differentiable at every point of , and , then for some with one auxiliary function, and this statement is that theorem at ; deriving it the other way round, from this statement to Cauchy's, is also possible but needs an auxiliary function of its own, so nothing is saved. What matters is that both rest on Rolle, and Rolle on the extreme value theorem.
-
The two hypotheses are on different sets on purpose. Continuity is asked for on the closed interval and differentiability only on the open one, so nothing at all is required of the difference quotients at and at . Weakening the continuity in step with the differentiability, so that both are asked for on only, destroys the theorem, which is exactly what on with is differentiable at every point of with , yet no satisfies , so continuity on the closed interval cannot be dropped from the mean value theorem ↗ shows on the companion page.
Depends on
Cauchy's mean value theorem: for continuous on with and differentiable on there is with ; no hypothesis on is needed in this product form
The derivative of at a point that is a limit point of , and differentiability on a set
Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point
Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
Intervals of : the nine order-convex forms, nondegeneracy, and length
The - limit of at a limit point of
Dependency tree · 2 levels
Sources
- Mean value theorem (Wikipedia)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 5 (Thm 5.10)
- J. Lebl, Basic Analysis I, §4.2
- J. Lebl, Basic Analysis I, Mean Value Theorem
- J. Hunter, An Introduction to Real Analysis