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

Functions of bounded variation form an algebra

Statement

If $f$ and $g$ have bounded variation on $[a, b]$ , so do $f + g$ , $c f$ , and $f g$ . If $∣ f ∣ \leq M_{f}$ and $∣ g ∣ \leq M_{g}$ , then

$Var (f g) \leq M_{f} Var (g) + M_{g} Var (f) .$

Facts & Assumptions

Given: BV functions $f, g : [a, b] \to R$ .

[L1]

BV functions are closed under sums and scalar multiples (Homogeneity and subadditivity of total variation).

[L2]

Every BV function is bounded (Total variation bounds increments; bounded-variation functions are bounded; zero variation means constant).

[L3]

Total variation is the supremum of partition sums (Bounded variation and total variation on an interval).

[L4]

Partitions and their finite sums are as in 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, and Laws of finite sums and finite products.

[L5]

Absolute value is multiplicative and satisfies the triangle inequality (Basic properties of the absolute value, The triangle inequality).

Proof

technique · direct

1.1

By [L2] choose $M_{f}, M_{g} \geq 0$ with $∣ f (x) ∣ \leq M_{f}$ and $∣ g (x) ∣ \leq M_{g}$ on $[a, b]$ . For a partition point pair $x < y$ , the identity $f (y) g (y) - f (x) g (x) = f (y) (g (y) - g (x)) + g (x) (f (y) - f (x))$ gives $∣ (f g) (y) - (f g) (x) ∣ \leq M_{f} ∣ g (y) - g (x) ∣ + M_{g} ∣ f (y) - f (x) ∣$ .

L2L5algebra

2.1

Summing step 1.1 over any partition yields $V (f g, P) \leq M_{f} V (g, P) + M_{g} V (f, P) \leq M_{f} Var (g) + M_{g} Var (f)$ . Taking the supremum proves the displayed bound and that $f g$ is BV.

step 1.1L3L4

3.1

Closure under sums and scalar multiples is [L1], and step 2.1 supplies closure under products, so the BV functions form an algebra under pointwise operations.

step 2.1L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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

William F. Trench, Introduction to Real Analysis, Ch. 3 (standard reference, not scraped)