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.

A continuous function of a Stieltjes-integrable function is Stieltjes integrable for a nondecreasing integrator

Statement

Suppose α:[a,b]R\alpha:[a,b]\to\mathbb R is nondecreasing, ff is bounded and Riemann–Stieltjes integrable with respect to α\alpha, and ϕ\phi is continuous on a compact interval containing f([a,b])f([a,b]). Then ϕf\phi\circ f is Riemann–Stieltjes integrable with respect to α\alpha.

Facts & Assumptions

Given: A nondecreasing α\alpha, a bounded fR(α)f\in R(\alpha), and a continuous ϕ\phi on a compact interval containing the range of ff.

[L1]

For a<ba<b, bounded ff and nondecreasing α\alpha, integrability in the mesh sense is equivalent to the conjunction of two conditions: ff is continuous at every discontinuity of α\alpha, and for every ε>0\varepsilon>0 some partition has i<nωi(f)Δiα<ε\sum_{i<n}\omega_i(f)\Delta_i\alpha<\varepsilon (Darboux criterion for Riemann–Stieltjes integrability with a nondecreasing integrator).

[L3]

Finite sums may be split and estimated termwise (Laws of finite sums and finite products).

Proof

technique · direct
1.1

Choose KK with ϕK|\phi|\le K. Given ε>0\varepsilon>0, uniform continuity supplies η>0\eta>0 such that uv<η|u-v|<\eta implies ϕ(u)ϕ(v)<ε/(2(1+α(b)α(a)))|\phi(u)-\phi(v)|<\varepsilon/(2(1+\alpha(b)-\alpha(a))).

L2
2.1

By [L1], choose a partition PP for which IoscI(f)ΔIα<ηε/(4K+1)\sum_I\operatorname{osc}_I(f)\,\Delta_I\alpha<\eta\varepsilon/(4K+1). Split its intervals into those with oscI(f)<η\operatorname{osc}_I(f)<\eta and the rest. The first class contributes less than ε/2\varepsilon/2 to the weighted oscillation sum of ϕf\phi\circ f. In the second class, oscI(ϕf)2K\operatorname{osc}_I(\phi\circ f)\le2K, while ηΔIαIoscI(f)ΔIα\eta\sum\Delta_I\alpha\le\sum_I\operatorname{osc}_I(f)\Delta_I\alpha; hence it too contributes less than ε/2\varepsilon/2.

step 1.1L1L2L3
3.1

Thus the weighted oscillation condition in [L1] holds for ϕf\phi\circ f. The same theorem says that ff is continuous at every discontinuity of α\alpha; continuity of ϕ\phi makes ϕf\phi\circ f continuous there as well. Both clauses of [L1] now give ϕfR(α)\phi\circ f\in R(\alpha).

step 2.1L1L2

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: 119 results over 16 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