Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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 bounded-variation function is uniformly approximable by step functions

Statement

If f:[a,b]Rf:[a,b]\to\mathbb R has bounded variation, then for every ε>0\varepsilon>0 there is a finite step function ss with fs<ε\lVert f-s\rVert_\infty<\varepsilon. Endpoint values of ss may be prescribed to equal those of ff.

More precisely, if E[a,b]E\subseteq[a,b] is at most countable and ff is continuous at every point of EE, the interior breakpoints of ss may all be chosen outside EE.

Facts & Assumptions

Given: A BV function ff, a tolerance ε>0\varepsilon>0, and, for the strengthened assertion, an at most countable set EE of continuity points of ff.

[L2]

Every nonempty subset of the reals that is bounded above has a supremum (Complete ordered field (least-upper-bound property)).

[L3]

Every nonempty open interval is uncountable (Every nondegenerate interval of R\mathbb{R} is uncountable).

Proof

technique · direct
1.1

Fix η>0\eta>0. Let AA be the set of x[a,b]x\in[a,b] for which there is a finite chain a=x0<<xm=xa=x_0<\cdots<x_m=x such that the oscillation of ff on every open interval (xj1,xj)(x_{j-1},x_j) is below η\eta. The set contains aa and is bounded above by bb, so c:=supAc:=\sup A exists by [L2].

L2construct
2.1

Suppose c<bc<b. The left limit at cc and the right limit at cc supplied by [L1] give one-sided intervals on which the oscillation is below η\eta. Choose xAx\in A in the left interval (use x=ax=a if c=ac=a), append cc to its chain if necessary, and then append a point y>cy>c in the right interval. This puts yy in AA, contradicting that cc is an upper bound. Hence c=bc=b. The left limit at bb now lets a chain ending sufficiently near bb be extended to bb. Thus there is a finite partition of [a,b][a,b] on each of whose open components the oscillation of ff is below η\eta. The singleton case is immediate.

step 1.1L1L2
3.1

On each open component choose one value of ff, and at every partition point assign the actual value of ff. The resulting finite step function differs from ff by less than η\eta everywhere. Taking η=ε/4\eta=\varepsilon/4 leaves room for the strengthened construction.

step 2.1choose
4.1

Only finitely many interior breakpoints lie in EE. Around each such breakpoint cc, continuity of ff gives a small two-sided interval, disjoint from the corresponding intervals for the other breakpoints, on which the oscillation is below ε/4\varepsilon/4. By [L3] choose a replacement point outside EE in that interval and between the neighboring breakpoints. Moving the breakpoint adds only a subinterval from this continuity neighborhood to either adjacent component; the original component oscillation is below ε/4\varepsilon/4, and a component can be enlarged at both ends, so its new oscillation is at most ε/4+ε/4+ε/4<ε\varepsilon/4+\varepsilon/4+\varepsilon/4<\varepsilon, the three pieces overlapping at the old breakpoints. Sampling again and retaining the actual values at all breakpoints and endpoints gives the required approximation with every interior breakpoint outside EE.

step 3.1L3

Depends on

Used by

Dependency tree · next 3 levels

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