Alphabeta Math
LemmaStatement: 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.

Total variation is additive over adjacent subintervals and decreases under restriction

Statement

If acba\le c\le b and f:[a,b]Rf:[a,b]\to\mathbb R, then ff has bounded variation on [a,b][a,b] if and only if its restrictions have bounded variation on [a,c][a,c] and [c,b][c,b]. In that case

Var[a,b](f)=Var[a,c](f)+Var[c,b](f).\operatorname{Var}_{[a,b]}(f)=\operatorname{Var}_{[a,c]}(f)+\operatorname{Var}_{[c,b]}(f).

Consequently restriction to any subinterval cannot increase total variation.

Facts & Assumptions

Given: Reals acba\le c\le b and a function f:[a,b]Rf:[a,b]\to\mathbb R.

[L1]

Total variation is the supremum of finite variation sums, and singleton variation is 00 (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:uxv}[u,v]=\{x:u\le x\le v\} (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct
1.1

Given partitions P1P_1 of [a,c][a,c] and P2P_2 of [c,b][c,b], splice their point lists at cc. The resulting partition PP of [a,b][a,b] satisfies V(f,P)=V(f,P1)+V(f,P2)V(f,P)=V(f,P_1)+V(f,P_2). Thus, whenever ff is BV on [a,b][a,b], each restriction is BV and Var[a,c](f)+Var[c,b](f)Var[a,b](f)\operatorname{Var}_{[a,c]}(f)+\operatorname{Var}_{[c,b]}(f)\le\operatorname{Var}_{[a,b]}(f). The assertion is unchanged when c=ac=a or c=bc=b, because the singleton term is 00.

L1L2L3L5
1.2

Conversely, insert cc into an arbitrary partition PP of [a,b][a,b]. The refined sum splits into a sum on [a,c][a,c] and one on [c,b][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)V(f,P)\le\operatorname{Var}_{[a,c]}(f)+\operatorname{Var}_{[c,b]}(f).

L1L2L3
2.1

Taking the supremum over PP 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][u,v]\subseteq[a,b] shows Var[u,v](f)Var[a,b](f)\operatorname{Var}_{[u,v]}(f)\le\operatorname{Var}_{[a,b]}(f).

step 1.1step 1.2L1L4L5

Depends on

Used by

Dependency tree · next 3 levels

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