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

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)\le g(x)$ and $N_f(x)\le h(x)$ for every $x$ .

Facts & Assumptions

Given: A function $f:[a,b]\to\mathbb 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 $\mathbb{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|\le |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)|\le(g(t_{i+1})-g(t_i))+(h(t_{i+1})-h(t_i))$ . Summing and telescoping gives $V(f,P)\le 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)\le g(x)+h(x)$ , while $f(x)-f(a)=g(x)-h(x)$ . Adding these inequalities and dividing by $2$ yields $P_f(x)\le g(x)$ ; subtracting the increment identity from the variation inequality yields $N_f(x)\le h(x)$ .

step 1.2L1L2algebra∎

Depends on

Used by

Dependency tree · next 3 levels

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

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)