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 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

Statement

If f:I→Rf:I\to\mathbb R is convex on an open interval, then f−′(c)f'_-(c) and f+′(c)f'_+(c) are finite for every c∈Ic\in I. Moreover, for u<vu<v in II,

f−′(u)≤f+′(u)≤f(v)−f(u)v−u≤f−′(v)≤f+′(v).f'_-(u)\le f'_+(u)\le\frac{f(v)-f(u)}{v-u}\le f'_-(v)\le f'_+(v).

Facts & Assumptions

Given: A convex f:I→Rf:I\to\mathbb R on an open interval and u<vu<v in II.

[L1]

For a convex function and three ordered points, the three secant slopes satisfy s(x,y)≤s(x,z)≤s(y,z)s(x,y)\le s(x,z)\le s(y,z) (For a convex function and x<y<zx<y<z, the three secant slopes satisfy s(x,y)≤s(x,z)≤s(y,z)s(x,y)\le s(x,z)\le s(y,z)).

[L2]

The left and right derivatives are the one-sided limits of the difference quotient (The left and right derivatives of a real function as one-sided limits of its difference quotient).

[L3]

A nondecreasing function on an interval has every well-posed one-sided limit, given by the corresponding supremum or infimum (One-sided limits of a monotone function always exist: for ff nondecreasing on an interval II and c∈Ic \in I, lim⁡x→c−f(x)=sup⁡{f(x):x∈I, x<c}\lim_{x \to c^{-}} f(x) = \sup\{f(x) : x \in I,\ x < c\} whenever II has points below cc, lim⁡x→c+f(x)=inf⁡{f(x):x∈I, x>c}\lim_{x \to c^{+}} f(x) = \inf\{f(x) : x \in I,\ x > c\} whenever it has points above cc, and these satisfy lim⁡x→c−f(x)≤f(c)≤lim⁡x→c+f(x)\lim_{x \to c^{-}} f(x) \le f(c) \le \lim_{x \to c^{+}} f(x)).

Proof

technique · direct
1.1

For fixed c∈Ic\in I, the functions x↦s(x,c)x\mapsto s(x,c) on x<cx<c and x↦s(c,x)x\mapsto s(c,x) on x>cx>c are nondecreasing by [L1]; choosing points on both sides of cc, [L1] bounds each near cc between two fixed finite outer secant slopes.

L1L2
2.1

The monotone one-sided-limit theorem [L3] therefore supplies finite one-sided limits of these two slope functions at cc, and [L2] identifies them respectively with f−′(c)f'_-(c) and f+′(c)f'_+(c).

step 1.1L2L3
3.1

Apply [L1] to x<u<vx<u<v and let x→u−x\to u^-, then to u<v<zu<v<z and let z→v+z\to v^+; together with s(u,v)≤f−′(v)s(u,v)\le f'_-(v) and f+′(u)≤s(u,v)f'_+(u)\le s(u,v) obtained in the same way, this gives the displayed chain.

step 1.1step 2.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

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