The Derivative and the Mean Value Theorems

About this page

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.

✓ 16 results · all verified · 13 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

1 · Prerequisites

Real Analysis

Set Theory

Topology

2 · Logical flowchart

3 · Items

The derivative f'(c) = lim_x → c f(x) - f(c)/x - c of f : A → ℝ at a point c ∈ A that is a limit point of A, and differentiability on a set

Carathéodory's characterisation: f is differentiable at c if and only if there is φ : A → ℝ, continuous at c, with f(x) - f(c) = φ(x)(x - c) for every x ∈ A, and then φ is unique and φ(c) = f'(c)

A function differentiable at c is continuous at c

The linear-approximation form of the derivative: f is differentiable at c with f'(c) = L if and only if the remainder r(x) = f(x) - f(c) - L(x-c) satisfies lim_x → c r(x)/(x-c) = 0; at most one L does so, so x ↦ f(c) + L(x-c) is the unique affine map approximating f to first order at c

Sums, scalar multiples, products and quotients: (f+g)'(c) = f'(c) + g'(c), (α f)'(c) = α f'(c), (fg)'(c) = f'(c)g(c) + f(c)g'(c), and (f/g)'(c) = (f'(c)g(c) - f(c)g'(c))/g(c)² when g(c) ≠ 0

For a natural n ≥ 1 the function x ↦ xⁿ is differentiable everywhere with derivative ι(n) x^ n-1; for n = 0 it is the constant 1, with derivative 0; for a natural n ≥ 1 the function x ↦ x⁻ⁿ is differentiable at every x ≠ 0 with derivative -ι(n) x⁻ⁿ⁻¹; consequently every polynomial function is differentiable at every real, with the derivative computed term by term

The chain rule, in one line from Carathéodory: if g is differentiable at c and f is differentiable at g(c), then f ∘ g is differentiable at c with (f ∘ g)'(c) = f'(g(c)) g'(c)

Derivative of an inverse: if f is continuous and injective on a nondegenerate interval I and differentiable at c ∈ I with f'(c) ≠ 0, then the inverse g is differentiable at f(c) with g'(f(c)) = 1/f'(c); and if f'(c) = 0 then g is not differentiable at f(c)

Local (relative) maximum and minimum of f : A → ℝ at a point, the strict forms, and what it means for the point to be interior to A

Fermat's interior extremum theorem: if f has a local extremum at a point c interior to its domain and is differentiable at c, then f'(c) = 0

Rolle's theorem: if a < b, f is continuous on [a,b], differentiable at every point of (a,b), and f(a) = f(b), then f'(c) = 0 for some c ∈ (a,b)

Cauchy's mean value theorem: for f, g continuous on [a,b] with a<b and differentiable on (a,b) there is c ∈ (a,b) with (f(b)-f(a))g'(c) = (g(b)-g(a))f'(c); no hypothesis on g' is needed in this product form

The mean value theorem, as the case g(x) = x of Cauchy's: for f continuous on [a,b] with a < b and differentiable on (a,b) there is c ∈ (a,b) with f(b) - f(a) = f'(c)(b-a)

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

On an interval I, for f continuous on I and differentiable at every interior point: f' ≥ 0 throughout gives f nondecreasing, f' > 0 gives f increasing, f' ≤ 0 and f' < 0 give the two decreasing forms; conversely a nondecreasing f has f' ≥ 0 and a nonincreasing f has f' ≤ 0 wherever it is differentiable, and no strict converse is claimed

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

What is fixed here and what is not: the derivative is taken at a point of the domain that is also a limit point of it, one-sided derivatives and derivatives of order above one are not introduced at this point in the reading order, and f'(c) and df/dx(c) name the same real number

False statement

FALSE: differentiability at every point of (a,b) alone yields a c ∈ (a,b) with f(b) - f(a) = f'(c)(b-a)

False statement

FALSE: if f'(c) = 0 then f is not increasing on any interval containing c

Sources