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.

Every slope between the left and right derivatives of a convex function gives a supporting line

Statement

Let f:I→Rf:I\to\mathbb R be convex on an open interval, let c∈Ic\in I, and let mm satisfy f−′(c)≤m≤f+′(c)f'_-(c)\le m\le f'_+(c). Then the line x↦f(c)+m(x−c)x\mapsto f(c)+m(x-c) supports ff at cc.

Facts & Assumptions

Given: A convex f:I→Rf:I\to\mathbb R, an interior point cc, and f−′(c)≤m≤f+′(c)f'_-(c)\le m\le f'_+(c).

[L1]

For u<vu<v, 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) (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]

A line of slope mm supports ff at cc when f(x)≥f(c)+m(x−c)f(x)\ge f(c)+m(x-c) throughout the interval (A supporting line of slope mm for a real function at an interior point).

Proof

technique · direct
1.1

If x<cx<c, [L1] applied to x<cx<c gives (f(c)−f(x))/(c−x)≤f−′(c)≤m(f(c)-f(x))/(c-x)\le f'_-(c)\le m.

L1L2
2.1

If x>cx>c, [L1] gives m≤f+′(c)≤(f(x)−f(c))/(x−c)m\le f'_+(c)\le(f(x)-f(c))/(x-c).

step 1.1L2algebra
3.1

Multiplying the inequalities in steps 1.1 and 2.1 by their positive denominators and rearranging yields f(x)≥f(c)+m(x−c)f(x)\ge f(c)+m(x-c) on both sides of cc, while equality holds at cc; hence [L2] applies.

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

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