Alphabeta Math
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 is additive over adjacent subintervals and decreases under restriction

Statement

If a≤c≤b and f:[a,b]→R, then f has bounded variation on [a,b] if and only if its restrictions have bounded variation on [a,c] and [c,b]. In that case

Var⁡[a,b](f)=Var⁡[a,c](f)+Var⁡[c,b](f).

Consequently restriction to any subinterval cannot increase total variation.

Facts & Assumptions

Given: Reals a≤c≤b and a function f:[a,b]→R.

[L1]

Total variation is the supremum of finite variation sums, and singleton variation is 0 (Bounded variation and total variation on an interval).

[L4]

A supremum is the least upper bound of a nonempty set bounded above, and is unique (Complete ordered field (least-upper-bound property), Suprema and infima are unique).

[L5]

Closed subintervals are the sets [u,v]={x:u≤x≤v} (Intervals of R: the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct
1.1L1L2L3L5

Given partitions P1 of [a,c] and P2 of [c,b], splice their point lists at c. The resulting partition P of [a,b] satisfies V(f,P)=V(f,P1)+V(f,P2). Thus, whenever f is BV on [a,b], each restriction is BV and Var⁡[a,c](f)+Var⁡[c,b](f)≤Var⁡[a,b](f). The assertion is unchanged when c=a or c=b, because the singleton term is 0.

1.2L1L2L3

Conversely, insert c into an arbitrary partition P of [a,b]. The refined sum splits into a sum on [a,c] and one on [c,b], while inserting a point does not decrease the sum, because the corresponding increment is replaced by two increments whose absolute values dominate it by the triangle inequality. Hence V(f,P)≤Var⁡[a,c](f)+Var⁡[c,b](f).

2.1step 1.1step 1.2L1L4L5∎

Taking the supremum over P in step 1.2 and combining it with step 1.1 proves the equality and the equivalence of boundedness. Applying the equality twice to [u,v]⊆[a,b] shows Var⁡[u,v](f)≤Var⁡[a,b](f).

Depends on

Dependency tree · 2 levels

Sources