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.
FALSE: if then is not increasing on any interval containing
Statement
False claim: let be an interval (Intervals of : the nine order-convex forms, nondegeneracy, and length), let and let be a point at which is differentiable with
(The derivative of at a point that is a limit point of , and differentiability on a set). Then is not 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.
Why it is tempting. 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 proves that at every interior point gives an increasing function, and one reads the implication backwards: if strict increase comes from a strictly positive derivative, surely a derivative that fails to be strictly positive somewhere must destroy the strict increase there. It does not. Claim 5 of that theorem is the true converse, and it is non-strict: an increasing has wherever it is differentiable, and nothing forbids equality at isolated points.
Facts & Assumptions
Given: The interval , the point and the function , (Integer powers , Intervals of : the nine order-convex forms, nondegeneracy, and length).
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, claim 2): for a natural the function is differentiable at every real with derivative .
Canonical naturals (The canonical natural of a field, Canonical naturals are positive and strictly increasing): for every natural , so in particular .
Powers (Integer powers ): , , and , so .
Order arithmetic (Sign rules for products and monotonicity of multiplication, Ordered field): a product of two positive reals is positive and a product of two negative reals is positive; the order is total and transitive, and trichotomy holds.
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): for order-convex and continuous on and differentiable at every interior point of with there, is increasing on .
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): is continuous at every point of its domain for every natural ; and continuity passes to a subset of the domain (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
Restriction of the derivative (The derivative of at a point that is a limit point of , and differentiability on a set): if , if is a limit point of and if is differentiable at , then is differentiable at with the same derivative; every point of an order-convex set with at least two elements is a limit point of it (Limit point, isolated point, adherent point, derived set, and dense subset of ); and a point is interior to a set exactly when for some real (The -neighbourhood and the punctured -neighbourhood of a point of , Interior, closure, boundary and exterior of a subset of ).
A positive base has positive natural powers (Monotonicity of and of , claim 1).
Refutation
By [L1] with , the function is differentiable at every real with . In particular by [L3].
For every real one has : if this is [L9]; if then is a product of two negative reals, hence positive by [L3] and [L4]. Therefore for every , being a product of two positive reals by [L2] and [L4].
Put and , both order-convex with at least two elements (Intervals of : the nine order-convex forms, nondegeneracy, and length). Every real is interior to , since ; and is not interior to , since every contains , which is not in . As every interior point of lies in and so satisfies , the interior points of are exactly the reals . The same argument gives that the interior points of are exactly the reals .
By [L6] the function is continuous on , hence is continuous on and is continuous on . At every interior point of one has by step 1.3, so is a limit point of by [L7] and is differentiable at with derivative by step 1.2 and [L7]. So [L5] gives that is increasing on ; the same argument on gives that is increasing on .
Let with . If then and step 2.1 gives . If then and step 2.1 gives . Otherwise and , so with gives , while with gives , and transitivity gives . The three cases are exhaustive, since failing both and means and . So is increasing on by [L8].
The false claim fails on this witness: is an interval, is differentiable at with by step 1.1, and yet is increasing on by step 3.1. So a vanishing derivative forbids nothing of the kind, and the claim is false.
Remarks
-
What survives. Claim 5 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 the correct converse and is non-strict: an increasing function differentiable at a point of its interval has there. This witness saturates that inequality at exactly one point, and no more can be said in general.
-
How large the vanishing set can be is not settled here. The witness has at a single point. Nothing on this page says how big the set may be for an increasing , and nothing here should be read as suggesting that it must be small.
-
The same function is the standard witness for a second false reading, that a vanishing derivative marks a local extremum: has neither a local maximum nor a local minimum at , precisely because it is increasing. 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 ↗ on the companion page computes the derivative in full and draws the further consequence, through 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 , that the inverse of this function is not differentiable at .
Depends on
- 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
- Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $\mathbb{R}$, with the dictionary to monotone sequences
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
- On an interval $I$, for $f$ continuous on $I$ and differentiable at every interior point: $f' \ge 0$ throughout gives $f$ nondecreasing, $f' > 0$ gives $f$ increasing, $f' \le 0$ and $f' < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f' \ge 0$ and a nonincreasing $f$ has $f' \le 0$ wherever it is differentiable, and no strict converse is claimed
- Integer powers $a^m$
- Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Sign rules for products and monotonicity of multiplication
- 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
- 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
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
- The $\varepsilon$-neighbourhood and the punctured $\varepsilon$-neighbourhood of a point of $\mathbb{R}$
- Interior, closure, boundary and exterior of a subset of $\mathbb{R}$
- Ordered field
- Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 93 results over 26 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Monotonic function (Wikipedia) (standard reference, not scraped)
- Stationary point (Wikipedia) (standard reference, not scraped)
- T. Gantumur, Differentiation (standard reference, not scraped)
- J. Hunter, An Introduction to Real Analysis (standard reference, not scraped)