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 Derivative and the Mean Value Theorems: Examples and Counterexamples
1 · Prerequisites
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Foundations of the Real Numbers for Analysis
- Limits of Real Functions
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Relations, Functions, and Quotients
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Suprema and Infima
- The Derivative and the Mean Value Theorems
- The ZFC Axioms and the Basic Set Constructions
- Topology of ℝ
2 · Summary
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Worked derivatives from the algebra of derivatives and the power rule: , and the quotient rule applied to on
Example
Numerals below denote canonical naturals of : is , is , and so on (The canonical natural of a field). Powers are those of Integer powers .
Claim 1. Let be given by
Then is differentiable at every (The derivative of at a point that is a limit point of , and differentiability on a set) and
Claim 2. Put and let be given by . Then every is a limit point of , is differentiable at as a function on , and
Nothing here is new: both computations are readings of Sums, scalar multiples, products and quotients: , , , and when on top of For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term. They are written out because the two places a computation of this kind goes wrong are the constant term, whose derivative is and not , and the domain of the quotient, which is not .
Facts & Assumptions
Given: The functions and of the statement, and an arbitrary real ; for claim 2 also .
Power rule (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term): for a natural the function is differentiable at every real with derivative ; and is the constant , with derivative (claims 1 and 2).
Algebra of derivatives (Sums, scalar multiples, products and quotients: , , , and when ): at a limit point of the common domain, sums, scalar multiples and products of functions differentiable at are differentiable at with the stated formulas; and if the denominator is nonzero at then, on , the point lies in and is a limit point of , and is differentiable at with derivative .
Canonical naturals (The canonical natural of a field, Canonical naturals are positive and strictly increasing): , and for naturals ; in particular and , the latter from .
Powers (Integer powers ): , and .
Every real is a limit point of , punctured neighbourhoods being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Verification
Let , a limit point of by [L5]. By [L1] the functions , and are differentiable at with derivatives , and respectively, using [L4].
Put and , both functions on , and let with .
Claim 1. The function is the sum of the scalar multiples , and , so by the sum and scalar-multiple rules of [L2] it is differentiable at with , the last step by [L3].
The functions and are differentiable at every real with and : is the sum of and the constant , whose derivatives at are and by [L1] and [L4]; and is the sum of and the constant .
Claim 2. By step 1.2 one has , and is exactly . So the quotient rule of [L2] applies: , the point is a limit point of , and is differentiable at with .
Expanding the numerator: , the last equality because by [L3]. So .
Both claims are verified: claim 1 by step 2.1 and claim 2 by steps 3.1 and 4.1.
Remarks
-
The constant term is where the index trap sits. Written informally, the derivative of "is" , and is undefined at . Claim 1 of For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term exists precisely so that the constant case is handled by its own statement, and the answer there is on the whole line.
-
The quotient lives on , not on . The function is not defined at , and no derivative of it there is asserted or could be. Sums, scalar multiples, products and quotients: , , , and when states its quotient case on the set where the denominator does not vanish for exactly this reason, and it also supplies the fact that the smaller set still has as a limit point, without which the derivative there would not be a defined symbol.
-
Reading the numerals. is what "" means as an element of ; the equality is a lemma (Canonical naturals are positive and strictly increasing) and not an act of arithmetic on the page. Every numeral in this library is such an image, and where a computation multiplies two of them the lemma is what licenses collapsing the product.
is continuous everywhere and not differentiable at : the difference quotient equals on the right and on the left, so the two one-sided limits differ
Statement refuted
Refuted claim: if , if is continuous at a point (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point) and if is a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ), then is differentiable at (The derivative of at a point that is a limit point of , and differentiability on a set).
This is the converse of A function differentiable at is continuous at , and it is false. The witness is on at : a single corner is enough, and the failure is visible in one line, the difference quotient taking the value to the right of and to the left.
Facts & Assumptions
Given: The set , the function , (Basic properties of the absolute value), and the point .
Continuity of the absolute value (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): the identity is continuous at every point of its domain (claim 5), and is continuous wherever is (claim 2); so is continuous at every point of (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
Derivative (The derivative of at a point that is a limit point of , and differentiability on a set): is a limit point of , punctured neighbourhoods being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ); the difference quotient of at is on ; and is differentiable at exactly when exists (The - limit of at a limit point of ).
Absolute value (Basic properties of the absolute value): ; for ; and for .
One-sided limits (The left and right limits of at , as limits of the restrictions of to and , Intervals of : the nine order-convex forms, nondegeneracy, and length): for and , the right limit of at is the limit at of restricted to , defined when is a limit point of that set, and the left limit is the same with .
Two-sided against one-sided (If is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree): if is a limit point of both and , then for every real the equality holds if and only if both one-sided limits at exist and equal .
At a limit point of its domain a function has at most one limit (At a limit point of the domain a function has at most one limit); and the limit of a constant function at a limit point of its domain is , any serving (The - limit of at a limit point of ).
: (The multiplicative identity is positive) gives , and trichotomy forbids equality.
Counterexample
is continuous at every point of , in particular at .
, so the difference quotient of at is on .
and , and is a limit point of each: for every real the point lies in with , and lies in with .
For one has , so ; for one has , so . Thus restricted to is the constant and restricted to is the constant .
By [L6] and step 1.3 the two restrictions have limits at , namely and ; so by [L4] the right limit of at is and the left limit is .
Suppose for some real . By step 1.3 the point is a limit point of both one-sided sets, so [L5] forces both one-sided limits to equal ; with step 3.1 and [L6] that gives and , hence , which [L7] forbids. So has no limit at , and by [L2] the function is not differentiable at .
The refuted claim therefore fails at , and : the point is a limit point of , is continuous at by step 1.1, and is not differentiable at by step 4.1.
Remarks
-
The failure is one-sided in a precise sense. Both one-sided limits of the difference quotient exist; they simply disagree. So this is not a function whose difference quotients oscillate or blow up, and the restriction of to is differentiable at with derivative , as The derivative of at a point that is a limit point of , and differentiability on a set records when it observes that differentiability is a property of the pair (function, domain).
-
What this says about A function differentiable at is continuous at . That implication is strict: continuity is genuinely weaker than differentiability, and this witness shows the gap opens at a single point of an otherwise unremarkable function. Nothing here suggests the gap is small in any other sense; how large the set of non-differentiability of a continuous function can be is not a question this page can pose.
-
Why the argument needs If is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree and not merely two computations. Two different one-sided values do not by themselves contradict anything until one knows that a two-sided limit would have to agree with both, and that is exactly what the cited theorem supplies, under the hypothesis that is approached from both sides inside the domain.
is increasing on although its derivative vanishes at , which is the witness for the false statement that a vanishing derivative forbids strict increase, and which makes its inverse non-differentiable at
Example
Let be (Integer powers ), with the canonical natural of The canonical natural of a field.
Claim 1. is differentiable at every with , and .
Claim 2. is increasing on , in the strict sense of Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of , with the dictionary to monotone sequences.
Claim 3. So the hypothesis " at every interior point" of claim 2 of On an interval , for continuous on and differentiable at every interior point: throughout gives nondecreasing, gives increasing, and give the two decreasing forms; conversely a nondecreasing has and a nonincreasing has wherever it is differentiable, and no strict converse is claimed is sufficient but not necessary for a function on an interval to be increasing; and the converse recorded there, claim 5, which gives only , cannot be strengthened to .
Claim 4. is continuous and injective on , so it has a continuous inverse on (Derivative of an inverse: if is continuous and injective on a nondegenerate interval and differentiable at with , then the inverse is differentiable at with ; and if then is not differentiable at ); and since , that inverse is not differentiable at .
Claims 1 and 2 are established in the refutation of FALSE: if then is not increasing on any interval containing and are quoted here; claims 3 and 4 are the two consequences worth drawing from them.
Facts & Assumptions
Given: The function , .
The refutation of FALSE: if then is not increasing on any interval containing establishes, for this : that is differentiable at every real with (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, The derivative of at a point that is a limit point of , and differentiability on a set); that ; and that is increasing on (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of , with the dictionary to monotone sequences).
is continuous at every point of its domain, for every natural (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, Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
is order-convex and has at least two elements (Intervals of : the nine order-convex forms, nondegeneracy, and length, Canonical naturals are positive and strictly increasing).
Derivative of an inverse (Derivative of an inverse: if is continuous and injective on a nondegenerate interval and differentiable at with , then the inverse is differentiable at with ; and if then is not differentiable at ): for order-convex with at least two elements and continuous and injective, with inverse , and for at which is differentiable, if then is not differentiable at .
Monotonicity from the derivative (On an interval , for continuous on and differentiable at every interior point: throughout gives nondecreasing, gives increasing, and give the two decreasing forms; conversely a nondecreasing has and a nonincreasing has wherever it is differentiable, and no strict converse is claimed): claim 2 says that at every interior point of an interval gives an increasing function, and claim 5 says that an increasing function differentiable at a limit point of the interval has there.
, since for every natural (Integer powers ).
Verification
Claims 1 and 2. By [L1] the function is differentiable at every with , its derivative at is , and is increasing on .
is injective by [L2], being increasing; it is continuous on by [L3]; and is order-convex with at least two elements by [L4]. So satisfies every hypothesis of [L5] with .
Claim 3. The hypothesis of claim 2 of [L6] fails for on , since is not positive, and yet the conclusion holds, being increasing on by step 1.1. So that hypothesis is sufficient and not necessary. Likewise the conclusion of claim 5 of [L6] is attained with equality at by step 1.1, so it cannot be strengthened to .
Claim 4. By step 2.1 the hypotheses of [L5] hold, and by step 1.1 the function is differentiable at with . So [L5] gives that the inverse is not differentiable at , which is by [L7].
All four claims are verified: claims 1 and 2 by step 1.1, claim 3 by step 2.2 and claim 4 by step 3.1.
Remarks
-
The set is not identified here, and nothing needs it to be. Derivative of an inverse: if is continuous and injective on a nondegenerate interval and differentiable at with , then the inverse is differentiable at with ; and if then is not differentiable at states its conclusion about the inverse on , whatever that set is; that , so that is the cube root on the whole line, would need a surjectivity argument this item does not make and does not use.
-
Two different false readings, one witness. That forbids strict increase is refuted by claim 2; that marks a local extremum is refuted by the same fact, since an increasing function has no local extremum at an interior point of its interval. The second reading is the converse of Fermat's interior extremum theorem: if has a local extremum at a point interior to its domain and is differentiable at , then , and this page records it here rather than as a separate false statement.
-
Where the inverse fails, and why it is not surprising. Claim 4 is not a defect of the inverse rule but a theorem: wherever the derivative of an injective continuous function vanishes, the inverse cannot be differentiable, because the chain rule would then give the identity a derivative of . The cube root at is the standard picture of that, a vertical tangent, and it is proved here without any picture.
The chain rule applied to and to , with the Carathéodory factor written out in closed form in the first case
Example
Numerals denote canonical naturals of (The canonical natural of a field) and powers are those of Integer powers .
Claim 1. Let be . Then is differentiable at every (The derivative of at a point that is a limit point of , and differentiability on a set) and
Claim 2. For the Carathéodory factor (Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and ) of at is the polynomial function
which satisfies for every , is continuous at , and has .
Claim 3. Let be . Then is differentiable at every and
Claim 2 is included because it makes the mechanism of the chain rule visible: the factor that the proof of The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with takes from Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and is, for a power, an explicit polynomial, and no auxiliary case distinction is hidden inside it.
Facts & Assumptions
Given: The functions , and of the statement, and an arbitrary real .
Chain rule (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with ): with , , , a limit point of at which is differentiable, and a limit point of at which is differentiable, the composite is differentiable at with .
Power rule (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, claims 1 and 2): for a natural , is differentiable at every real with derivative ; and is the constant , of derivative .
Algebra of derivatives (Sums, scalar multiples, products and quotients: , , , and when , claims 1 and 2): sums and scalar multiples of functions differentiable at a limit point of the common domain are differentiable there, with the corresponding derivatives.
Carathéodory's characterisation (Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and ): is differentiable at a limit point of its domain if and only if some continuous at satisfies throughout, and then ; the factor is unique.
Factorisation of a difference of powers (Factorisation of , and the resulting Lipschitz estimate): for reals and a natural , (Finite sums and finite products, by recursion).
Finite sums (Laws of finite sums and finite products, claim 2): for a constant ; and powers combine as for (Laws of integer exponents).
Polynomial functions are continuous at every point of their domain (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, Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
Canonical naturals (The canonical natural of a field, Canonical naturals are positive and strictly increasing): for naturals , so , and ; and .
Every real is a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Verification
Put and , both on . By [L2] and [L3] the function is differentiable at every real with , and is differentiable at every real with .
Put , and , all on . By [L2] and [L3], , and at every real argument.
Claim 2. Fix and put for . Applying [L5] with , and gives for every real . As a finite sum of scalar multiples of powers of , the function is a polynomial function and so is continuous at by [L7]. Finally by [L6]. So is the factor of [L4] for at , and [L4] returns , in agreement with step 1.1.
Claim 1. By [L9] every real is a limit point of , and maps into , so [L1] applies to at any : is differentiable at with , the last step by [L8].
Claim 3. By [L1] and [L9], applied first to and then to , the function is differentiable at every real , with and then , the collapsing of the numerals by [L8].
The three claims are verified: claim 1 by step 2.2, claim 2 by step 2.1 and claim 3 by step 2.3.
Remarks
-
The closed form of the factor is what makes claim 2 worth stating. For a general the Carathéodory factor is produced by Carathéodory's characterisation: is differentiable at if and only if there is , continuous at , with for every , and then is unique and out of the difference quotient itself, and its value at the base point is filled in by hand; for a power it is a polynomial written down in advance, by Factorisation of , and the resulting Lipschitz estimate, and its continuity is then a reading of 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 rather than an appeal to the derivative. The two routes agree, which is step 2.1.
-
Nested composites cost nothing extra. Claim 3 applies The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with twice, and at each application the inner function maps into , so the hypothesis that the image point is a limit point of the outer domain is automatic. On a smaller domain it would not be, and that is the hypothesis a careless nesting would drop.
-
What the numerals hide. is an identity of canonical naturals (Canonical naturals are positive and strictly increasing), not an arithmetic fact about the symbol ; every collapse of a product of numerals above is that lemma.
For a natural , the derivative of on is , obtained from the inverse rule applied to ; in particular
Example
Let with , let be the canonical natural of The canonical natural of a field, and let rational powers be those of Rational powers of a positive base, so that is the unique nonnegative -th root of (Existence and uniqueness of -th roots: a unique with ).
Claim. The function
is differentiable at every (The derivative of at a point that is a limit point of , and differentiability on a set), and
In particular at , writing ,
The domain is and not , and the reason depends on . For the exponent is a negative rational, and Rational powers of a positive base leaves undefined for rational , so at the displayed formula is not a statement at all; and the root really is not differentiable there, by claim 2 of Derivative of an inverse: if is continuous and injective on a nondegenerate interval and differentiable at with , then the inverse is differentiable at with ; and if then is not differentiable at applied on , since has derivative at for (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Integer powers ). At neither obstruction arises: the exponent is , not negative; is the identity (Existence and uniqueness of -th roots: a unique with ); and the formula reads , which is correct at every real. So for the restriction to is a convenience of the uniform statement rather than a necessity. Nothing below asserts anything about the root at in either case.
Facts & Assumptions
Given: A natural , the set , the function , , and the function , .
Roots (Existence and uniqueness of -th roots: a unique with ): for every real and every natural there is a unique real with , written ; and when . By Rational powers of a positive base the rational power is that same number.
Rational power laws (Laws of rational exponents): for and rationals one has , , and ; and rational powers extend integer powers on positive bases (Rational powers of a positive base, Integer powers ).
Monotonicity of integer powers (Monotonicity of and of ): for a natural the map is strictly increasing on , hence injective there (claim 2); and implies (claim 1).
Continuity (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, and Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point): is continuous at every point of its domain, and continuity passes to a subset of the domain.
Power rule and restriction (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, claim 2, with the restriction clause of The derivative of at a point that is a limit point of , and differentiability on a set): on is differentiable at every real with derivative , and if lies in a subset of having as a limit point then the restriction is differentiable there with the same derivative.
Derivative of an inverse (Derivative of an inverse: if is continuous and injective on a nondegenerate interval and differentiable at with , then the inverse is differentiable at with ; and if then is not differentiable at , claim 1): for order-convex with at least two elements and continuous and injective with inverse , if is differentiable at with then is differentiable at with .
The continuous inverse theorem (Continuous inverse theorem: a continuous injective on an interval is a bijection onto the order-convex set , and the inverse is continuous and strictly monotone in the same sense as ): is a bijection with a unique two-sided inverse; and a right inverse of a bijection is that unique inverse (Injection, surjection, bijection).
is order-convex with at least two elements (Intervals of : the nine order-convex forms, nondegeneracy, and length), and every point of it is a limit point of it (The derivative of at a point that is a limit point of , and differentiability on a set, Limit point, isolated point, adherent point, derived set, and dense subset of ); and , hence , for (Canonical naturals are positive and strictly increasing).
Verification
is order-convex with at least two elements, and every point of is a limit point of .
is injective on by [L3], continuous on by [L4], and takes only positive values by [L3].
. For one has by [L3], so ; and for the number is positive by [L1], hence lies in , and by [L1], so .
The map , , is the inverse of . By [L7] and step 1.2 that bijection has a unique two-sided inverse; by step 1.3 the map takes values in and satisfies for every , so it is a right inverse of the bijection and therefore is that unique inverse.
is differentiable at every with , by [L5] together with step 1.1; and , since by [L8] and by [L3] as .
Let and put , an element of by [L1], with by [L1]. By step 1.2, step 2.2 and [L6], applied on at , the inverse is differentiable at with .
Rewriting in terms of : since and is a natural, [L2] gives , a positive real. Hence , using from [L2] and from [L8].
At the map is , and step 4.1 reads , again by [L2].
Remarks
-
Why the inverse rule and not a direct estimate. A direct computation of has to rationalise the numerator using the factorisation of a difference of -th powers, and then has to know that to evaluate the limit, which is the continuity of the root. Derivative of an inverse: if is continuous and injective on a nondegenerate interval and differentiable at with , then the inverse is differentiable at with ; and if then is not differentiable at packages both, and its own proof gets the continuity from Continuous inverse theorem: a continuous injective on an interval is a bijection onto the order-convex set , and the inverse is continuous and strictly monotone in the same sense as rather than proving it again.
-
Where the hypothesis is spent. At the derivative is positive, so the hypothesis costs nothing on . It is exactly the hypothesis that fails at when the domain is enlarged to and , and there the inverse rule says the root is not differentiable at , which is claim 2 of that theorem.
-
The exponent arithmetic is rational arithmetic, not real arithmetic. The identity is an identity of rationals, and is claim 5 of Laws of rational exponents. Real exponents are not available at this page's position in the reading order, so every step above stays inside as Rational powers of a positive base requires. The later Real powers for positive bases, with the zero-base positive-exponent convention ↗ does not alter this proof boundary.
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
Statement refuted
Refuted claim: let with and let be 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 .
That is The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with with the hypothesis of continuity on deleted, and it is false; the false statement itself is recorded as FALSE: differentiability at every point of alone yields a with . This item works the witness out: it locates the failure at a single point, measures it, and shows that repairing that one value restores the conclusion.
Facts & Assumptions
Given: The function with for and , and the identity , (Intervals of : the nine order-convex forms, nondegeneracy, and length).
The refutation of FALSE: differentiability at every point of alone yields a with establishes, for this : that is differentiable at every with ; that , so ; and that no satisfies .
One-sided limits (The left and right limits of at , as limits of the restrictions of to and , Intervals of : the nine order-convex forms, nondegeneracy, and length): the left limit of at is the limit at of restricted to , defined when is a limit point of that set; the right limit is the same with .
The limit condition (The - limit of at a limit point of ): means that for every real there is a real such that every in the domain of with satisfies . The clause removes from the quantifier (Basic properties of the absolute value, The -neighbourhood and the punctured -neighbourhood of a point of ).
Continuity at a limit point (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point, clause 1): for a limit point of , the function is continuous at if and only if exists and equals .
Mean value theorem (The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with ) and Rolle's theorem (Rolle's theorem: if , is continuous on , differentiable at every point of , and , then for some ), both of which additionally require continuity on the closed interval.
The identity on is continuous on and differentiable at every point of with derivative , its difference quotient at any being the constant (The derivative of at a point that is a limit point of , and differentiability on a set, The - limit of at a limit point of , Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
, since (The multiplicative identity is positive).
Counterexample
By [L1] the function is differentiable at every with , satisfies , and admits no with . So the refuted claim fails at , .
The point is a limit point of and of : for every real the point satisfies , hence , and .
, the limit taken over the domain . Given a real , take ; every with has by [L3], hence and , so . Since the same quantifier ranges over the same points when the domain is cut down to , this also says by [L2]. The right limit at is not defined, since is empty and is therefore not a limit point of it.
is not continuous at . By step 1.2 the point is a limit point of , so [L4] makes continuity there equivalent to ; by step 2.1 the left side is and by [L1] the right side is , and by [L7]. So exactly one hypothesis of [L5] fails, at exactly one point, and it is the deleted one.
The repair. The identity agrees with at every point of except , where and . By [L6] the function is continuous on and differentiable at every point of with , so [L5] applies to ; and indeed for every . So moving the single value back to turns a function with no admissible into one for which every is admissible.
The same witness refutes the corresponding weakening of Rolle's theorem: by step 1.1, and yet at every by step 1.1 and [L7]. So neither theorem in [L5] survives the deletion of continuity on the closed interval.
Remarks
-
The discontinuity is of the mildest possible kind. Both of the quantities that exist at , the left limit and the value, exist and are finite; they simply differ. In the vocabulary of the page on monotone functions and discontinuities this is a removable discontinuity, and step 4.1 removes it. Nothing pathological is needed to break the mean value theorem.
-
Why the derivative sees nothing. The difference quotient of at an interior is evaluated only at points within of , and every such point lies in , where is the identity. So carries no information at all about , while the conclusion of the mean value theorem is an equation containing . Continuity on the closed interval is precisely the bridge between the two.
-
Reflecting the witness covers the other endpoint. The function is differentiable at every point of with the same constant derivative and fails continuity at instead of at , so nothing is special about which endpoint is broken.
The identity on attains its maximum at and its minimum at with derivative at both, so Fermat's theorem genuinely needs the extremum to be at an interior point
Statement refuted
Refuted claim: let , let and let be a limit point of at which has a local extremum (Local (relative) maximum and minimum of at a point, the strict forms, and what it means for the point to be interior to ) and is differentiable (The derivative of at a point that is a limit point of , and differentiability on a set). Then .
That is Fermat's interior extremum theorem: if has a local extremum at a point interior to its domain and is differentiable at , then with the hypothesis " is interior to " deleted and replaced by the weaker one needed for to be a defined symbol at all. It is false: the identity on attains a greatest and a least value, both at points of the domain that are not interior to it, and its derivative is everywhere.
Facts & Assumptions
Given: The set (Intervals of : the nine order-convex forms, nondegeneracy, and length) and the function , .
Derivative of the identity (The derivative of at a point that is a limit point of , and differentiability on a set, The - limit of at a limit point of ): every point of the order-convex set , which has at least two elements, is a limit point of it (Limit point, isolated point, adherent point, derived set, and dense subset of ); and the difference quotient of at any is at every with , a constant function whose limit at is . So is differentiable at every with .
Local extrema (Local (relative) maximum and minimum of at a point, the strict forms, and what it means for the point to be interior to ): has a local maximum at when for every for some real , and a local minimum with the inequality reversed; a value that is a greatest value of over the whole of is a local maximum, and a least value is a local minimum (claim 4 of its body); and is interior to exactly when for some real (Interior, closure, boundary and exterior of a subset of , The -neighbourhood and the punctured -neighbourhood of a point of ).
Maximum and minimum of a set (Maximum and minimum of a set): is a maximum of when and for every , and a minimum when and for every .
Fermat's interior extremum theorem (Fermat's interior extremum theorem: if has a local extremum at a point interior to its domain and is differentiable at , then ) additionally requires to be interior to .
, since (The multiplicative identity is positive).
Counterexample
By [L1] the function is differentiable at every , and ; in particular , and every point of is a limit point of .
Every satisfies , so and ; and . So is a maximum of and is a minimum of by [L3], and by [L2] the function has a local maximum at and a local minimum at , hence a local extremum at each.
Neither nor is interior to : for every real the point lies in and not in , and the point lies in and not in . So no around either point is contained in .
The refuted claim therefore fails at : the point lies in and is a limit point of by step 1.1, has a local extremum there by step 1.2 and is differentiable there by step 1.1, and yet by [L5]. The same holds at .
Nothing in [L4] is contradicted. By step 1.3 neither nor is interior to , so the hypothesis of that theorem is not met at either point, and the deleted hypothesis is exactly the one that fails. Indeed no point of at all carries a vanishing derivative, and consistently with [L4] no interior point of carries a local extremum: by step 1.2 the only extrema of over sit at the two endpoints.
Remarks
-
What the endpoint case would need instead. At the domain supplies points on the left only, and the difference quotient there is positive, so the most one can conclude is . That one-sided refinement is not stated at this point in the reading order, since nothing here uses it; the point of the witness is only that the two-sided conclusion is unavailable.
-
The witness is not delicate. Any function increasing on and differentiable there whose derivative vanishes at neither endpoint does the same job, and the identity is chosen for having a derivative that can be computed from The derivative of at a point that is a limit point of , and differentiability on a set in one line. The nonvanishing clause has to be said and is not automatic: is increasing on and differentiable there, and attains its least value at , yet , so it refutes nothing at the left endpoint. What removing interiority destroys is the guarantee that the derivative vanishes, not the possibility. So the failure at an endpoint is the generic situation and not an artefact.
-
Why this matters for Rolle's theorem. Rolle's theorem: if , is continuous on , differentiable at every point of , and , then for some produces an interior point precisely by ruling this case out: when both extrema sit at the endpoints, the hypothesis forces the function to be constant, and any interior point then serves. Without that hypothesis the endpoint case is exactly the one that survives, and the identity on is it.
The mean value theorem gives for , so the square root is Lipschitz with constant on
Example
Write for the nonnegative square root (Existence and uniqueness of -th roots: a unique with , Rational powers of a positive base) and for the canonical natural (The canonical natural of a field).
Claim. Let and let , . Then
so is Lipschitz with constant on (Lipschitz map, -Hölder map for rational , and contraction, clause 3 of Dictionary: for with the metric , continuity and uniform continuity of agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of is compact in the open-cover sense of exactly when it is a compact metric subspace) and hence uniformly continuous on (Uniform continuity of : one serving every pair of points of ).
The constant is what the derivative bound gives, and the domain is what makes the bound available. On the derivative of is at most ; on it is not bounded at all, and the companion counterexample on this page shows that there the Lipschitz conclusion fails.
Facts & Assumptions
Given: The set , order-convex with at least two elements (Intervals of : the nine order-convex forms, nondegeneracy, and length), and the function , .
Derivative of the square root (For a natural , the derivative of on is , obtained from the inverse rule applied to ; in particular , at ): the map on is differentiable at every with derivative .
Restriction of the domain (The derivative of at a point that is a limit point of , and differentiability on a set): , every point of is a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of , Intervals of : the nine order-convex forms, nondegeneracy, and length), and a function differentiable at such a point remains differentiable there after restriction, with the same derivative.
A function differentiable at a point is continuous there (A function differentiable at is continuous at ).
Rational powers (Laws of rational exponents, Monotonicity of and of , Existence and uniqueness of -th roots: a unique with ): for ; ; , since and and the nonnegative square root is unique; and for rational , implies (claim 3 of the monotonicity lemma).
Order arithmetic (Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication, Canonical naturals are positive and strictly increasing, Multiplying inequalities of positives): , so and ; gives (Inverses of positives are positive, and reciprocation reverses order); a product of two positive reals is positive (Sign rules for products and monotonicity of multiplication); and the NONSTRICT multiplication of inequalities between nonnegatives, and imply , is Multiplying inequalities of positives and is not stated by Sign rules for products and monotonicity of multiplication, whose multiplicative claims are strict. Also for (Basic properties of the absolute value).
Interiority (Interior, closure, boundary and exterior of a subset of , The -neighbourhood and the punctured -neighbourhood of a point of ): is interior to exactly when for some real .
Bounded derivative gives Lipschitz (If is continuous on an interval and at every interior point, then for all , so is Lipschitz with constant and uniformly continuous on ): for order-convex, continuous on and differentiable at every interior point of , and a real with at every interior point, one has for all ; such an is Lipschitz with constant and uniformly continuous on (Lipschitz map, -Hölder map for rational , and contraction, Dictionary: for with the metric , continuity and uniform continuity of agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of is compact in the open-cover sense of exactly when it is a compact metric subspace, Uniform continuity of : one serving every pair of points of ).
Verification
The interior points of are exactly the reals . For the neighbourhood is contained in , so is interior; the point is not interior, since and for every real ; and every interior point of lies in , hence is .
For every real one has . If then by [L4], so . If then by [L4], and , so by [L4] and [L5].
By [L1] and [L2] the function is differentiable at every with , and by [L3] it is continuous at every point of , hence continuous on .
At every interior point of one has by step 1.1, so by [L4] and by step 1.2; multiplying the pair and as in [L5] gives by step 2.1, and therefore by [L5].
Apply [L7] with , and , a real by [L5]: the hypotheses hold by step 2.1 for the continuity and differentiability and by step 3.1 for the bound, so for all , that is ; is Lipschitz with constant on ; and is uniformly continuous on .
Remarks
-
Why the bound is and not something smaller. The supremum of over is approached at , where , and the argument uses nothing sharper than . No claim is made that is the least Lipschitz constant on ; the corollary produces one constant that works, which is all the statement asserts.
-
Everything depends on the left endpoint being and not . The bound is exactly the statement , read through the monotonicity of rational powers. On the same expression is unbounded, and on is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped on this page shows the conclusion then fails outright, so the hypothesis of If is continuous on an interval and at every interior point, then for all , so is Lipschitz with constant and uniformly continuous on is doing real work here.
-
The mean value theorem is inside the corollary, not applied directly. If is continuous on an interval and at every interior point, then for all , so is Lipschitz with constant and uniformly continuous on is one application of The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with on the segment joining and ; quoting the packaged form avoids repeating the segment argument and, more importantly, avoids restating the endpoint conventions each time.
on is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped
Statement refuted
Refuted claim: let be order-convex (Intervals of : the nine order-convex forms, nondegeneracy, and length) and let be continuous on and differentiable at every interior point of (The derivative of at a point that is a limit point of , and differentiability on a set). Then is Lipschitz on , that is, there is a real with for all (Lipschitz map, -Hölder map for rational , and contraction, clause 3 of Dictionary: for with the metric , continuity and uniform continuity of agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of is compact in the open-cover sense of exactly when it is a compact metric subspace).
That is If is continuous on an interval and at every interior point, then for all , so is Lipschitz with constant and uniformly continuous on with the hypothesis deleted. It is false, and the witness is the square root on : an interval on which the derivative exists at every interior point and is bounded above by no real.
Facts & Assumptions
Given: The set , order-convex with at least two elements (Intervals of : the nine order-convex forms, nondegeneracy, and length), and the function , , the nonnegative square root (Existence and uniqueness of -th roots: a unique with , Rational powers of a positive base); numerals denote canonical naturals (The canonical natural of a field).
Derivative of the square root (For a natural , the derivative of on is , obtained from the inverse rule applied to ; in particular , at , with the restriction clause of The derivative of at a point that is a limit point of , and differentiability on a set and ): is differentiable at every with , every point of being a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ).
A function differentiable at a point is continuous there (A function differentiable at is continuous at ).
Uniqueness of the nonnegative square root (Existence and uniqueness of -th roots: a unique with ): for there is exactly one with , and it is (Rational powers of a positive base, Integer powers ).
Rational powers (Laws of rational exponents, Monotonicity of and of ): for ; ; ; and for rational , implies (claim 2 of the monotonicity lemma).
Archimedean property in reciprocal form (For every in a complete ordered field there is a natural with , Every complete ordered field is Archimedean): for every real there is a natural with .
Order and numeral arithmetic (Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication, Multiplying inequalities of positives, Canonical naturals are positive and strictly increasing, Monotonicity of and of , Basic properties of the absolute value, The canonical natural of a field): for ; gives (Inverses of positives are positive, and reciprocation reverses order); a product of positives is positive and multiplying a STRICT inequality by a positive real preserves it (Sign rules for products and monotonicity of multiplication); the NONSTRICT form, and imply , is not stated by Sign rules for products and monotonicity of multiplication, whose multiplicative claims are strict, but by Multiplying inequalities of positives, and it is what licenses both multiplying a by a positive real and dividing a by one, the divisor entering as its positive inverse; gives (Monotonicity of and of , claim 2); for (Basic properties of the absolute value); and and for naturals , so , and .
Interiority and boundedness (Interior, closure, boundary and exterior of a subset of , The -neighbourhood and the punctured -neighbourhood of a point of , Lower bound, bounded below, bounded set): is interior to exactly when for some real ; and a set of reals is bounded above when some real exceeds or equals all of its elements.
The corollary under test (If is continuous on an interval and at every interior point, then for all , so is Lipschitz with constant and uniformly continuous on ) additionally requires a real with at every interior point.
Counterexample
By [L1] the function is differentiable at every with , using [L4] and [L6]; and by [L2] it is continuous at every point of , hence continuous on .
The interior points of are exactly the reals with : for such a the neighbourhood with lies in ; the point is not interior, since and for every real ; and every interior point lies in .
The derivative is bounded above by no real. Let be a real. If , any with has by step 1.1. If , put , a positive real, and use [L5] to fix a natural with ; put , so and . By [L4], , so by [L6], and hence . So for every real there is an interior point of with , and the set of values of on the interior of is bounded above by no real.
is not Lipschitz on . Suppose some real satisfied for all . Let be a real with , and put and . Then , so ; and and by [L3], since with and with . Hence and by [L6], and the supposition gives ; dividing by gives for every such . Taking shows , so . Now use [L5] to fix a natural with and put , a real with ; then , contradicting . So no such exists.
The refuted claim therefore fails at and : by step 1.1 the function is continuous on the order-convex set and differentiable at every point of , in particular at every interior point of by step 1.2, and yet by step 2.2 it is not Lipschitz on . Nothing in [L8] is contradicted: by step 2.1 no real bounds on the interior of , so the hypothesis deleted from that corollary is exactly the one that fails.
Remarks
-
The two failures are separate statements, and both are proved. That the derivative is unbounded (step 2.1) does not by itself refute the claim, since the claim is about a Lipschitz bound and not about ; and the Lipschitz bound is refuted directly, by a pair of points whose square roots differ by while the points themselves differ by . Only step 2.1 is needed to say which hypothesis of If is continuous on an interval and at every interior point, then for all , so is Lipschitz with constant and uniformly continuous on is the one that fails.
-
Contrast with the same function on . There the derivative is bounded by and the corollary applies, which is The mean value theorem gives for , so the square root is Lipschitz with constant on on this page. The function is the same; the interval is what decides. That is the sense in which the Lipschitz property is a property of the pair (function, domain), exactly as Uniform continuity of : one serving every pair of points of records for uniform continuity.
-
What is not claimed. This item asserts the failure of the Lipschitz condition on and nothing more. In particular nothing above says whether is uniformly continuous on , nor whether it satisfies a Hölder condition of some exponent below there; those are separate questions, and no item on this page is entitled to be cited for either.
With and on the quotient form is meaningless because , while the product form of Cauchy's theorem still holds
Statement refuted
Refuted claim: 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) and differentiable at every point of (The derivative of at a point that is a limit point of , and differentiability on a set). Then there is with
This is the shape in which Cauchy's mean value theorem is usually remembered, and it is not what Cauchy's mean value theorem: for continuous on with and differentiable on there is with ; no hypothesis on is needed in this product form says. It is false as stated, because under the hypotheses given neither quotient need be a real number at all. The witness below makes both denominators vanish.
Facts & Assumptions
Given: The reals and and the functions with and (Integer powers , Intervals of : the nine order-convex forms, nondegeneracy, and length); numerals denote canonical naturals (The canonical natural of a field).
Power rule and restriction (For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, claim 2, and The derivative of at a point that is a limit point of , and differentiability on a set): on is differentiable at every real with derivative ; every point of the order-convex set , which has at least two elements, is a limit point of it (Limit point, isolated point, adherent point, derived set, and dense subset of , Intervals of : the nine order-convex forms, nondegeneracy, and length); and a function differentiable at such a point stays differentiable there after restriction, with the same derivative.
Continuity (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, Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point): is continuous at every point of its domain.
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), in its product form: under the hypotheses above there is with .
Rolle's theorem (Rolle's theorem: if , is continuous on , differentiable at every point of , and , then for some ): a function continuous on , differentiable at every point of and taking equal values at the endpoints has a vanishing derivative somewhere in .
Signs and powers (Integer powers , Sign rules for products and monotonicity of multiplication, Monotonicity of and of ): the recursion with gives , the product of two negatives being positive (Sign rules for products and monotonicity of multiplication), and ; that for every natural is claim 4 of Monotonicity of and of and is not read off Integer powers .
Canonical naturals (The canonical natural of a field, Canonical naturals are positive and strictly increasing): , and for ; in particular , so .
Division by is not defined: has no multiplicative inverse in a field (Field).
Counterexample
By [L2] both and are continuous on , and by [L1] both are differentiable at every , with and , using [L5] for . So the pair satisfies every hypothesis of the refuted claim, and of [L3], with and .
By [L5], , , and . Hence and .
The left-hand side of the refuted claim names no real number: its denominator is by step 1.2, and has no inverse by [L7]. So there is no for which the asserted equation holds, since the equation cannot even be formed; the claim fails on this pair.
The right-hand side fails as well at one point of the interval: by step 1.1, so the quotient is undefined at , again by [L7].
The product form is untouched. By [L3] there is with , which by steps 1.1 and 1.2 reads , that is ; since by [L6], this forces . And does lie in and does satisfy the identity, both sides being . So [L3] holds on this pair, with its only admissible point.
The vanishing of is not an accident of the choice. By step 1.2 one has , so [L4] already forces to vanish at some point of , and by step 2.3 that point is , the same point the product form produces. So on this pair every quotient the refuted claim writes down is undefined, while [L3] is satisfied; the quotient form needs hypotheses the product form does not, and as stated it is false.
Remarks
-
What the quotient form would need. Two extra hypotheses, and they are of different kinds: , a condition on the endpoints, and at the point produced, a condition on a point one does not choose. The second is the awkward one, since the theorem hands back a and says nothing about it. This is why 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 stated as a product identity in this library, with no hypothesis on at all.
-
A cheaper repair than a hypothesis on . If then, by Rolle's theorem: if , is continuous on , differentiable at every point of , and , then for some read contrapositively, nothing forces to vanish; and the product identity may then be divided by to give , which is a true statement with no division by anywhere. That is the form worth remembering.
-
The witness is the smallest natural one. is even and the interval is symmetric about , which is the whole of the mechanism; any even on a symmetric interval does the same. The choice only makes nonzero, so that the failure is not hidden by both sides vanishing for a trivial reason.
Sources
Standard references
Recommended treatments; not extraction sources.
- Power rule (Wikipedia)
- Quotient rule (Wikipedia)
- J. Lebl, Basic Analysis I, The Derivative
- Absolute value (Wikipedia)
- Differentiable function (Wikipedia)
- J. Lebl, Basic Analysis I, §4.1
- T. Gantumur, Differentiation
- Stationary point (Wikipedia)
- Monotonic function (Wikipedia)
- Inverse function rule (Wikipedia)
- J. Hunter, An Introduction to Real Analysis
- Chain rule (Wikipedia)
- Nth root (Wikipedia)
- Mean value theorem (Wikipedia)
- Rolle's theorem (Wikipedia)
- Classification of discontinuities (Wikipedia)
- J. Lebl, Basic Analysis I, Mean Value Theorem
- Fermat's theorem (stationary points) (Wikipedia)
- Maximum and minimum (Wikipedia)
- Lipschitz continuity (Wikipedia)
- Square root (Wikipedia)
- Archimedean property (Wikipedia)
- MIT 18.785 Number Theory I, Lecture 19