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.

A continuous midpoint-convex function on an interval is convex

Statement

If $f : I \to R$ is midpoint convex and continuous on an interval $I$ , then $f$ is convex on $I$ .

Facts & Assumptions

Given: A continuous midpoint-convex $f : I \to R$ , points $x, y \in I$ , and $λ \in [0, 1]$ .

[L1]

Midpoint convexity gives the convexity inequality at every dyadic weight $k / 2^{n}$ (Midpoint convexity gives the convexity inequality at every dyadic weight $k / 2^{n}$ ).

[L2]

For every positive real $ε$ , there is a natural number $n \geq 1$ such that $1 / n < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L3]

For every real $r$ there is an integer $k$ with $k \leq r < k + 1$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

Proof

technique · direct

1.1

For every $n$ , [L3] applied to $2^{n} λ$ supplies $k_{n}$ with $k_{n} / 2^{n} \leq λ < (k_{n} + 1) / 2^{n}$ ; the elementary induction $2^{n} \geq n + 1$ and [L2] show $k_{n} / 2^{n} \to λ$ .

L1L2L3

2.1

Apply [L1] at the dyadic weight $k_{n} / 2^{n}$ and let $n \to \infty$ . Continuity of $f$ at $λ x + (1 - λ) y$ and ordinary limit laws give the convexity inequality at $λ$ .

step 1.1L2algebra

3.1

At $λ = 0$ and $λ = 1$ the inequality is equality; with step 2.1 this proves convexity for every weight in $[0, 1]$ .

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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