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.

The jumps of a variation function equal the absolute jumps of the original function

Statement

Let $f : [a, b] \to R$ have bounded variation and let $V_{f} (x) = {Var}_{[a, x]} (f)$ . At an interior point $c$ ,

$V_{f} (c +) - V_{f} (c) = ∣ f (c +) - f (c) ∣, V_{f} (c) - V_{f} (c -) = ∣ f (c) - f (c -) ∣ .$

The corresponding one-sided formula holds at either endpoint. In particular, $V_{f}$ is continuous at every point where $f$ is continuous.

Facts & Assumptions

Given: A bounded-variation function $f : [a, b] \to R$ , its variation function $V_{f}$ , and a point $c \in [a, b]$ .

[L1]

$V_{f} (y) - V_{f} (x) = {Var}_{[x, y]} (f)$ whenever $x \leq y$ (Total variation is additive over adjacent subintervals and decreases under restriction).

[L2]

$∣ f (y) - f (x) ∣ \leq {Var}_{[x, y]} (f)$ (Total variation bounds increments; bounded-variation functions are bounded; zero variation means constant).

[L3]

Every relevant one-sided limit of a BV function exists (A bounded-variation function has at most countably many discontinuities, all of the first kind, The left and right limits of $f$ at $c$ , as limits of the restrictions of $f$ to $A \cap (- \infty, c)$ and $A \cap (c, \infty)$ ).

[L4]

Finite sums and differences preserve existing one-sided limits (Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero).

[L5]

Continuity is equality of the relevant limit with the function value (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

[L6]

A bounded nondecreasing sequence converges; its partial sums are therefore Cauchy, so the sums over all sufficiently remote finite tails are uniformly small (A monotone sequence converges if and only if it is bounded, Series, partial sums, convergence and the sum, divergence, and the tail series, A series converges iff each of its tail series converges, and the sum splits as $s_{N}$ plus the $N$ -th tail, Every convergent sequence is Cauchy).

[L7]

Geometric sequences with ratio in $(0, 1)$ tend to zero (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

Proof

technique · direct

1.1

Since $V_{f}$ is nondecreasing and bounded above by $V_{f} (b)$ , its one-sided limits exist. By [L1] and [L2], $V_{f} (x) - V_{f} (c) \geq ∣ f (x) - f (c) ∣$ for $x > c$ ; passage to the right limit gives $V_{f} (c +) - V_{f} (c) \geq ∣ f (c +) - f (c) ∣$ .

L1L2L3L4

1.2

For the reverse inequality, fix $x_{0} > c$ and put $x_{n} = c + (x_{0} - c) 2^{- n}$ . Let $a_{n} = {Var}_{[x_{n + 1}, x_{n}]} (f)$ . By repeated additivity, every partial sum of the nonnegative series $\sum_{n} a_{n}$ is ${Var}_{[x_{N}, x_{0}]} (f)$ for a suitable $N$ , hence is bounded by ${Var}_{[c, x_{0}]} (f)$ . Its tails therefore tend to zero by [L6], while $x_{n} ↓ c$ by [L7].

L1L6L7

2.1

Given $ε > 0$ , take $N$ so large that the series tail from $N$ is below $ε$ and $∣ f (y) - f (c +) ∣ < ε$ whenever $c < y \leq x_{N}$ . For any partition $c = t_{0} < t_{1} < \dots < t_{k} = x_{N}$ , choose $m \geq N$ with $x_{m + 1} < t_{1} \leq x_{m}$ . The part after its first increment is at most [step 1.2, L1, L2, L3, L6] ${Var}_{[t_{1}, x_{N}]} (f) \leq {Var}_{[x_{m + 1}, x_{N}]} (f) = \sum_{n = N}^{m} a_{n} < ε,$ while $∣ f (t_{1}) - f (c) ∣ \leq ∣ f (c +) - f (c) ∣ + ε$ . Taking the supremum over partitions gives ${Var}_{[c, x_{N}]} (f) \leq ∣ f (c +) - f (c) ∣ + 2 ε$ . Restriction gives the same bound for $c < x \leq x_{N}$ , and [L2] gives the reverse bound in the limit.

3.1

Thus $\lim_{x ↓ c} {Var}_{[c, x]} (f) = ∣ f (c +) - f (c) ∣$ , and [L1] proves the right-hand formula. Applying steps 1.2–2.1 to the reversed interval proves the left-hand formula. If $f$ is continuous at $c$ , both absolute jumps vanish by [L5], so $V_{f}$ is continuous there. Endpoint cases use only the available side.

step 1.1step 2.1L1L3L5∎

Depends on

Used by

Dependency tree · two levels

64 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)