TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02

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.

A differentiable function on an open interval is convex if and only if its derivative is nondecreasing

Statement

For a differentiable $f : I \to R$ on an open interval $I$ , $f$ is convex if and only if $f^{'}$ is nondecreasing on $I$ .

Facts & Assumptions

Given: A differentiable $f : I \to R$ on an open interval $I$ .

[L1]

For a convex function, the ordered one-sided-derivative chain holds; at a differentiability point its two one-sided derivatives equal the ordinary derivative (A convex function on an open interval has finite left and right derivatives everywhere, with $f_{-}^{'} (u) \leq f_{+}^{'} (u) \leq (f (v) - f (u)) / (v - u) \leq f_{-}^{'} (v) \leq f_{+}^{'} (v)$ for $u < v$ ).

[L2]

If a differentiable real function has nonnegative derivative on an interval, then it is nondecreasing on that interval (On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed).

Proof

technique · cases

1.1

Assume $f$ is convex. For $u < v$ , [L1] becomes $f^{'} (u) \leq f^{'} (v)$ , so $f^{'}$ is nondecreasing.

assume-case forwardL1

1.2

Assume instead that $f^{'}$ is nondecreasing. For a fixed $c$ , the derivative of $g (x) = f (x) - f^{'} (c) x$ is nonpositive on the left of $c$ and nonnegative on the right; apply [L2] to $- g$ on the left and to $g$ on the right to obtain $f (x) \geq f (c) + f^{'} (c) (x - c)$ for every $x \in I$ .

assume-case reverseL2algebra

2.1

If $z = λ x + (1 - λ) y$ , multiply the supporting inequalities of step 1.2 at $z$ for $x$ and $y$ by $λ$ and $1 - λ$ and add; this gives $f (z) \leq λ f (x) + (1 - λ) f (y)$ . Thus the two cases prove the equivalence.

step 1.1step 1.2cases-exhaustive∎

Depends on

Used by

Dependency tree · two levels

29 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

R. Gardner, Convex Functions, Notes 6.6 (standard reference, not scraped)