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.

Total variation bounds increments; bounded-variation functions are bounded; zero variation means constant

Statement

Let $f:[a,b]\to\mathbb R$ have bounded variation. Then

$|f(y)-f(x)|\le\operatorname{Var}_{[a,b]}(f)$ for all $x,y\in[a,b]$ ;
$f$ is bounded on $[a,b]$ ;
$\operatorname{Var}_{[a,b]}(f)=0$ if and only if $f$ is constant.

These claims include the singleton interval $a=b$ .

Facts & Assumptions

Given: Reals $a\le b$ and a bounded-variation function $f:[a,b]\to\mathbb R$ .

[L1]

Total variation is the supremum of the partition sums $V(f,P)$ , with value $0$ on a singleton interval (Bounded variation and total variation on an interval).

[L2]

A point of an interval can be inserted into a partition without deleting its existing points (Partition of $[a,b]$ as a finite strictly increasing list $a = t_0 < t_1 < \dots < t_n = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).

[L3]

Finite sums of nonnegative terms dominate every term (Laws of finite sums and finite products).

[L4]

$|u+v|\le |u|+|v|$ in an ordered field (The triangle inequality).

[L5]

A subset of $\mathbb R$ is bounded when the absolute values of its members have a common real bound (Lower bound, bounded below, bounded set).

Proof

technique · direct

1.1

If $a<b$ and $x<y$ lie in $[a,b]$ , insert $x$ and $y$ into the endpoint partition. The resulting partition sum contains $|f(y)-f(x)|$ as a nonnegative term, so $|f(y)-f(x)|\le V(f,P)\le\operatorname{Var}_{[a,b]}(f)$ . The same inequality is $0\le\operatorname{Var}_{[a,b]}(f)$ when $x=y$ , and when $a=b$ only that case occurs.

L1L2L3

2.1

Put $M:=|f(a)|+\operatorname{Var}_{[a,b]}(f)$ . For $x\in[a,b]$ , $|f(x)|\le |f(x)-f(a)|+|f(a)|\le M$ , so $f([a,b])$ is bounded.

step 1.1L4L5

3.1

If the total variation is $0$ , step 1.1 gives $|f(y)-f(x)|=0$ for every $x,y$ , hence $f$ is constant. Conversely, if $f$ is constant then every increment in every partition sum is $0$ , so every sum and its supremum are $0$ ; the singleton convention gives the same conclusion when $a=b$ .

step 1.1L1L3∎

Depends on

Used by

Dependency tree · next 3 levels

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

William F. Trench, Introduction to Real Analysis, Ch. 3 (standard reference, not scraped)