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

Functions of bounded variation form an algebra

Statement

If ff and gg have bounded variation on [a,b][a,b], so do f+gf+g, cfcf, and fgfg. If ∣f∣≤Mf|f|\le M_f and ∣g∣≤Mg|g|\le M_g, then

Var⁡(fg)≤MfVar⁡(g)+MgVar⁡(f).\operatorname{Var}(fg)\le M_f\operatorname{Var}(g)+M_g\operatorname{Var}(f).

Facts & Assumptions

Given: BV functions f,g:[a,b]→Rf,g:[a,b]\to\mathbb 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][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, 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 Mf,Mg≥0M_f,M_g\ge0 with ∣f(x)∣≤Mf|f(x)|\le M_f and ∣g(x)∣≤Mg|g(x)|\le M_g on [a,b][a,b]. For a partition point pair x<yx<y, the identity f(y)g(y)−f(x)g(x)=f(y)(g(y)−g(x))+g(x)(f(y)−f(x))f(y)g(y)-f(x)g(x)=f(y)(g(y)-g(x))+g(x)(f(y)-f(x)) gives ∣(fg)(y)−(fg)(x)∣≤Mf∣g(y)−g(x)∣+Mg∣f(y)−f(x)∣|(fg)(y)-(fg)(x)|\le M_f|g(y)-g(x)|+M_g|f(y)-f(x)|.

L2L5algebra
2.1

Summing step 1.1 over any partition yields V(fg,P)≤MfV(g,P)+MgV(f,P)≤MfVar⁡(g)+MgVar⁡(f)V(fg,P)\le M_fV(g,P)+M_gV(f,P)\le M_f\operatorname{Var}(g)+M_g\operatorname{Var}(f). Taking the supremum proves the displayed bound and that fgfg 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 · next 3 levels

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