TheoremStatement: 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.

Jordan decomposition for functions of bounded variation

Statement

A real function $f$ on $[a, b]$ has bounded variation if and only if it is a difference of two nondecreasing functions. If $f (a) = 0$ , the canonical normalized decomposition is $f = P_{f} - N_{f}$ . More generally $f = f (a) + P_{f} - N_{f}$ .

It is minimal: if $f = f (a) + g - h$ with nondecreasing $g, h$ and $g (a) = h (a) = 0$ , then $P_{f} (x) \leq g (x)$ and $N_{f} (x) \leq h (x)$ for every $x$ .

Facts & Assumptions

Given: A function $f : [a, b] \to R$ .

[L1]

For BV $f$ , $P_{f}, N_{f}$ are nondecreasing, normalized at $a$ , and $f = f (a) + P_{f} - N_{f}$ (The positive and negative variations are nondecreasing and give the Jordan identities).

[L2]

Total variation is the supremum of sums of absolute increments (Bounded variation and total variation on an interval).

[L3]

Nondecreasing means that each forward increment is nonnegative (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences).

[L4]

A partition is a finite increasing point list (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).

[L5]

Finite sums telescope and distribute over addition (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L6]

$∣ u - v ∣ \leq ∣ u ∣ + ∣ v ∣$ (The triangle inequality).

Proof

technique · direct

1.1

If $f$ is BV, [L1] immediately supplies the stated difference of nondecreasing functions, with the asserted normalization.

1.2

Conversely suppose $f = f (a) + g - h$ with $g, h$ nondecreasing. For a partition $P = (n, t)$ , every forward increment of $g$ and $h$ is nonnegative, so $∣ f (t_{i + 1}) - f (t_{i}) ∣ \leq (g (t_{i + 1}) - g (t_{i})) + (h (t_{i + 1}) - h (t_{i}))$ . Summing and telescoping gives $V (f, P) \leq g (b) - g (a) + h (b) - h (a)$ , independent of $P$ ; hence $f$ is BV.

L2L3L4L5L6

2.1

Now assume the decomposition is normalized. On $[a, x]$ , step 1.2 gives $V_{f} (x) \leq g (x) + h (x)$ , while $f (x) - f (a) = g (x) - h (x)$ . Adding these inequalities and dividing by $2$ yields $P_{f} (x) \leq g (x)$ ; subtracting the increment identity from the variation inequality yields $N_{f} (x) \leq h (x)$ .

step 1.2L1L2algebra∎

Depends on

Used by

Dependency tree · two levels

36 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

Christopher Heil, Absolute Continuity and the Banach-Zaretsky Theorem (standard reference, not scraped)
William F. Trench, Introduction to Real Analysis, Ch. 3 (standard reference, not scraped)