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.

Homogeneity and subadditivity of total variation

Statement

For bounded-variation functions f,g:[a,b]→Rf,g:[a,b]\to\mathbb R and c∈Rc\in\mathbb R,

Var⁡(cf)=∣c∣Var⁡(f),Var⁡(f+g)≤Var⁡(f)+Var⁡(g).\operatorname{Var}(cf)=|c|\operatorname{Var}(f),\qquad \operatorname{Var}(f+g)\le\operatorname{Var}(f)+\operatorname{Var}(g).

Thus −f-f, f+gf+g, and every finite linear combination of BV functions are BV; in particular Var⁡(−f)=Var⁡(f)\operatorname{Var}(-f)=\operatorname{Var}(f).

Facts & Assumptions

Given: BV functions f,g:[a,b]→Rf,g:[a,b]\to\mathbb R and a scalar cc.

[L1]

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

[L2]

A partition is a finite increasing point list (Partition of [a,b][a,b] as a finite strictly increasing list a=t0<t1<⋯<tn=ba = t_0 < t_1 < \dots < t_n = b, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).

[L3]

Finite sums distribute over scalar multiplication and addition (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L4]

∣cu∣=∣c∣∣u∣|cu|=|c||u| (Basic properties of the absolute value).

[L5]

∣u+v∣≤∣u∣+∣v∣|u+v|\le|u|+|v| (The triangle inequality).

Proof

technique · direct
1.1

For every partition PP, [L4] and [L3] give V(cf,P)=∣c∣V(f,P)V(cf,P)=|c|V(f,P). Taking suprema gives Var⁡(cf)=∣c∣Var⁡(f)\operatorname{Var}(cf)=|c|\operatorname{Var}(f), including c=0c=0 and the singleton interval.

L1L2L3L4
1.2

For every partition, [L5] applied to each increment and then [L3] give V(f+g,P)≤V(f,P)+V(g,P)≤Var⁡(f)+Var⁡(g)V(f+g,P)\le V(f,P)+V(g,P)\le\operatorname{Var}(f)+\operatorname{Var}(g). Taking the supremum proves subadditivity.

L1L2L3L5
2.1

Step 1.1 with c=−1c=-1 gives Var⁡(−f)=Var⁡(f)\operatorname{Var}(-f)=\operatorname{Var}(f). Repeated use of steps 1.1 and 1.2 proves closure under every finite linear combination.

step 1.1step 1.2L3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 47 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