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.
Convex functions have countable supporting line representations
Statement
Let be finite and convex. For each define . Then for every real . This is a countable family with deterministic real coefficients; the coefficients need not be rational. The function is locally Lipschitz and Borel measurable.
Facts & Assumptions
Given: A finite convex function .
The finite one-sided derivatives bound secant slopes and are ordered at ordered points. (A convex function on an open interval has finite left and right derivatives everywhere, with for )
A slope between the one-sided derivatives defines a supporting line. (Every slope between the left and right derivatives of a convex function gives a supporting line)
The rational contact points form a countable set. ( is countably infinite)
Rational points approximate each real point arbitrarily closely. (The rationals embed densely in the reals)
A continuous real function is Borel measurable. (A continuous map has Borel preimages of Borel sets)
Proof
By [F1], is finite and lies between and . Therefore [F2] gives for every , with equality at . The family is countable by [F3], and no slope choice is made.
Fix real . For , the inequalities in [F1], also applied between and , bound the secant slope between the finite numbers and . The same bounds hold for for . Let be the maximum of their absolute values. Then , proving Lipschitz continuity on and thus continuity everywhere; [F5] gives Borel measurability.
For fixed use step 1.2 on . Given , [F4] supplies rational in this interval with . Then . Thus the supremum of the supporting lines is at least for every positive , and at most by step 1.1, proving equality. This also handles and affine functions with irrational slopes.
Source notes
Durrett Theorem 4.1.10 and countability remark, printed p.211, motivate the countable-support method. Here rational contact points with real slopes avoid any rational-coefficient ambiguity; the exact local supporting-line and derivative interfaces give the complete derivation.
Depends on
- Every slope between the left and right derivatives of a convex function gives a supporting line
- A convex function on an open interval has finite left and right derivatives everywhere, with $f'_-(u)\le f'_+(u)\le (f(v)-f(u))/(v-u)\le f'_-(v)\le f'_+(v)$ for $u<v$
- $\mathbb{Q}$ is countably infinite
- The rationals embed densely in the reals
- A continuous map has Borel preimages of Borel sets
Used by
Dependency tree · two levels
37 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
- Durrett, Probability: Theory and Examples, 5th ed. (standard reference, not scraped)