Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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→Rf:I\to\mathbb R on an open interval II, ff is convex if and only if f′f' is nondecreasing on II.

Facts & Assumptions

Given: A differentiable f:I→Rf:I\to\mathbb R on an open interval II.

[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)≤f+′(u)≤(f(v)−f(u))/(v−u)≤f−′(v)≤f+′(v)f'_-(u)\le f'_+(u)\le (f(v)-f(u))/(v-u)\le f'_-(v)\le f'_+(v) for u<vu<v).

[L2]

If a differentiable real function has nonnegative derivative on an interval, then it is nondecreasing on that interval (On an interval II, for ff continuous on II and differentiable at every interior point: f′≥0f' \ge 0 throughout gives ff nondecreasing, f′>0f' > 0 gives ff increasing, f′≤0f' \le 0 and f′<0f' < 0 give the two decreasing forms; conversely a nondecreasing ff has f′≥0f' \ge 0 and a nonincreasing ff has f′≤0f' \le 0 wherever it is differentiable, and no strict converse is claimed).

Proof

technique · cases
1.1

Assume ff is convex. For u<vu<v, [L1] becomes f′(u)≤f′(v)f'(u)\le f'(v), so f′f' is nondecreasing.

assume-case forwardL1
1.2

Assume instead that f′f' is nondecreasing. For a fixed cc, the derivative of g(x)=f(x)−f′(c)xg(x)=f(x)-f'(c)x is nonpositive on the left of cc and nonnegative on the right; apply [L2] to −g-g on the left and to gg on the right to obtain f(x)≥f(c)+f′(c)(x−c)f(x)\ge f(c)+f'(c)(x-c) for every x∈Ix\in I.

assume-case reverseL2algebra
2.1

If z=λx+(1−λ)yz=\lambda x+(1-\lambda)y, multiply the supporting inequalities of step 1.2 at zz for xx and yy by λ\lambda and 1−λ1-\lambda and add; this gives f(z)≤λf(x)+(1−λ)f(y)f(z)\le\lambda f(x)+(1-\lambda)f(y). Thus the two cases prove the equivalence.

step 1.1step 1.2cases-exhaustive∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 67 results over 19 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