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 $f, g$ continuous on $[a,b]$ with $a<b$ and differentiable on $(a,b)$ there is $c \in (a,b)$ with $\bigl(f(b)-f(a)\bigr)g'(c) = \bigl(g(b)-g(a)\bigr)f'(c)$; no hypothesis on $g'$ is needed in this product form
- The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$, and differentiability on a set
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ 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 $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- The $\varepsilon$-$\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$
Used by
- Conditional flow-matching training and exact-flow sampling Algorithm
- A function continuous on an interval I whose derivative vanishes at every interior point of I is constant on I; consequently two such functions with the same derivative differ by a constant Corollary
- A regular C¹ path has a C¹ arc-length reparametrization with derivative of Euclidean norm one Corollary
- An everywhere-positive-definite Hessian implies strict convexity Corollary
- Classical Neumann solutions differ by componentwise constants Corollary
- If f is continuous on an interval I and |f'| ≤ M at every interior point, then |f(x) - f(y)| ≤ M|x-y| for all x,y ∈ I, so f is Lipschitz with constant M and uniformly continuous on I Corollary
- Interior gradient bound for Poisson solutions Corollary
- Polynomial and exponential minimax estimation rates Corollary
- Strong convergence of subcritical powers Corollary
- The constructed classical solutions are locally determined by the Cauchy data Corollary
- The integral logarithm is continuous and strictly increasing on (0,∞) Corollary
- The Lax shock inequalities for convex scalar laws Corollary
- The spherical complementary series converge to the trivial representation Corollary
- A complete manifold with zero global injectivity radius Counterexample
- A non-Dini continuous Poisson source can destroy the continuity of the second derivatives Counterexample
- A strictly convex function can have a singular Hessian Counterexample
- An optimized mean-field law can lose posterior correlation Counterexample
- f(t) = (t², t³) on [0,1]: no ξ satisfies f(1)-f(0) = f'(ξ) Counterexample
- f(x) = x on [0,1) with f(1) = 0 is differentiable at every point of (0,1) with f' ≡ 1, yet no c satisfies f(1) - f(0) = f'(c), so continuity on the closed interval cannot be dropped from the mean value theorem Counterexample
- Point evaluation is unbounded below the Sobolev continuity threshold Counterexample
- The exponential is not uniformly continuous on ℝ Counterexample
- The final-time face is not part of the parabolic boundary Counterexample
- The heat flow need not converge in supremum norm Counterexample
- Banach algebra valued contour integral Definition
- Chebyshev weighted spectral Sobolev scale and projection Definition
- Kullback–Leibler divergence Definition
- Legendre weighted spectral-Sobolev scale and projection Definition
- The Logan-Shepp-Vershik-Kerov limit profile Ω Definition
- A Caputo startup singularity and a graded-grid calculation Example
- A damped Newton step precedes the local quadratic phase Example
- A dissipative electromechanical toy model under slow-fast blocking Example
- A finite Bernoulli large-deviation tail Example
- A finite-matrix Schrödinger split preserves norm Example
- A globally Lipschitz Hamiltonian force Example
- A Hopf--Lax solution with a forming corner from smooth data Example
- A one-parameter density prior meets the logarithmic contraction conditions Example
- A regularized logistic finite sum with an exact minimizer Example
- A wide tanh network stays lazy on a fixed time horizon Example
- Boundary-incompatible forcing reduces Strang order to five quarters in a Dirichlet modal model Example
- Endpoint sensor times are D-optimal for an intercept-slope model Example
…and 219 more results.
Dependency tree · two levels
26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Mean value theorem (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 5 (Thm 5.10) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §4.2 (standard reference, not scraped)
- J. Lebl, Basic Analysis I, Mean Value Theorem (standard reference, not scraped)
- J. Hunter, An Introduction to Real Analysis (standard reference, not scraped)