LemmaStatement: Literature-sourcedProof: AI-generatedprecheck 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 R$ have bounded variation. Then

$∣ f (y) - f (x) ∣ \leq {Var}_{[a, b]} (f)$ for all $x, y \in [a, b]$ ;
$f$ is bounded on $[a, b]$ ;
${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 \leq b$ and a bounded-variation function $f : [a, b] \to 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 ∣ \leq ∣ u ∣ + ∣ v ∣$ in an ordered field (The triangle inequality).

[L5]

A subset of $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) ∣ \leq V (f, P) \leq {Var}_{[a, b]} (f)$ . The same inequality is $0 \leq {Var}_{[a, b]} (f)$ when $x = y$ , and when $a = b$ only that case occurs.

L1L2L3

2.1

Put $M : = ∣ f (a) ∣ + {Var}_{[a, b]} (f)$ . For $x \in [a, b]$ , $∣ f (x) ∣ \leq ∣ f (x) - f (a) ∣ + ∣ f (a) ∣ \leq 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 · two levels

28 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

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