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 continuous midpoint-convex function on an interval is convex

Statement

If f:I→Rf:I\to\mathbb R is midpoint convex and continuous on an interval II, then ff is convex on II.

Facts & Assumptions

Given: A continuous midpoint-convex f:I→Rf:I\to\mathbb R, points x,y∈Ix,y\in I, and λ∈[0,1]\lambda\in[0,1].

[L1]

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

[L2]

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

[L3]

For every real rr there is an integer kk with k≤r<k+1k\le r<k+1 (Integer part: for every real xx there is exactly one integer mm with m≤x<m+1m \le x < m + 1).

Proof

technique · direct
1.1

For every nn, [L3] applied to 2nλ2^n\lambda supplies knk_n with kn/2n≤λ<(kn+1)/2nk_n/2^n\le\lambda<(k_n+1)/2^n; the elementary induction 2n≥n+12^n\ge n+1 and [L2] show kn/2n→λk_n/2^n\to\lambda.

L1L2L3
2.1

Apply [L1] at the dyadic weight kn/2nk_n/2^n and let n→∞n\to\infty. Continuity of ff at λx+(1−λ)y\lambda x+(1-\lambda)y and ordinary limit laws give the convexity inequality at λ\lambda.

step 1.1L2algebra
3.1

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

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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