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 and , then has bounded variation on if and only if its restrictions have bounded variation on and . In that case
Consequently restriction to any subinterval cannot increase total variation.
Facts & Assumptions
Given: Reals and a function .
Total variation is the supremum of finite variation sums, and singleton variation is (Bounded variation and total variation on an interval).
A partition is a finite strictly increasing endpoint list, and a refinement contains every point of the original partition (Partition of as a finite strictly increasing list , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).
Finite sums telescope and split at an index (Finite sums and finite products, by recursion, Laws of finite sums and finite products).
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).
Closed subintervals are the sets (Intervals of : the nine order-convex forms, nondegeneracy, and length).
Proof
Given partitions of and of , splice their point lists at . The resulting partition of satisfies . Thus, whenever is BV on , each restriction is BV and . The assertion is unchanged when or , because the singleton term is .
Conversely, insert into an arbitrary partition of . The refined sum splits into a sum on and one on , 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 .
Taking the supremum over in step 1.2 and combining it with step 1.1 proves the equality and the equivalence of boundedness. Applying the equality twice to shows .
Depends on
- Bounded variation and total variation on an interval
- 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
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- Complete ordered field (least-upper-bound property)
- Suprema and infima are unique
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
Used by
- Variation function and positive and negative variations Definition
- Refinement and tag-change estimates for Stieltjes sums Lemma
- The jumps of a variation function equal the absolute jumps of the original function Lemma
- The positive and negative variations are nondecreasing and give the Jordan identities Lemma
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
- William F. Trench, Introduction to Real Analysis, Ch. 3 (standard reference, not scraped)