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.

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

Statement

Let $f : I \to R$ be convex on an open interval, let $c \in I$ , and let $m$ satisfy $f_{-}^{'} (c) \leq m \leq f_{+}^{'} (c)$ . Then the line $x \mapsto f (c) + m (x - c)$ supports $f$ at $c$ .

Facts & Assumptions

Given: A convex $f : I \to R$ , an interior point $c$ , and $f_{-}^{'} (c) \leq m \leq f_{+}^{'} (c)$ .

[L1]

For $u < v$ , $f_{-}^{'} (u) \leq f_{+}^{'} (u) \leq (f (v) - f (u)) / (v - u) \leq f_{-}^{'} (v) \leq f_{+}^{'} (v)$ (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]

A line of slope $m$ supports $f$ at $c$ when $f (x) \geq f (c) + m (x - c)$ throughout the interval (A supporting line of slope $m$ for a real function at an interior point).

Proof

technique · direct

1.1

If $x < c$ , [L1] applied to $x < c$ gives $(f (c) - f (x)) / (c - x) \leq f_{-}^{'} (c) \leq m$ .

L1L2

2.1

If $x > c$ , [L1] gives $m \leq f_{+}^{'} (c) \leq (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) \geq f (c) + m (x - c)$ on both sides of $c$ , while equality holds at $c$ ; hence [L2] applies.

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · two levels

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