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 is nondecreasing, is bounded and Riemann–Stieltjes integrable with respect to , and is continuous on a compact interval containing . Then is Riemann–Stieltjes integrable with respect to .
Facts & Assumptions
Given: A nondecreasing , a bounded , and a continuous on a compact interval containing the range of .
For , bounded and nondecreasing , integrability in the mesh sense is equivalent to the conjunction of two conditions: is continuous at every discontinuity of , and for every some partition has (Darboux criterion for Riemann–Stieltjes integrability with a nondecreasing integrator).
The function is bounded and uniformly continuous on its compact domain (A continuous real function on a compact subset of is bounded, Heine-Cantor in : a continuous real function on a compact subset of is uniformly continuous, proved -natively from sequential compactness).
Finite sums may be split and estimated termwise (Laws of finite sums and finite products).
Proof
Choose with . Given , uniform continuity supplies such that implies .
By [L1], choose a partition for which . Split its intervals into those with and the rest. The first class contributes less than to the weighted oscillation sum of . In the second class, , while ; hence it too contributes less than .
Thus the weighted oscillation condition in [L1] holds for . The same theorem says that is continuous at every discontinuity of ; continuity of makes continuous there as well. Both clauses of [L1] now give .
Depends on
- Darboux criterion for Riemann–Stieltjes integrability with a nondecreasing integrator
- Riemann–Stieltjes sums, upper and lower sums, and the Riemann–Stieltjes integral
- Heine-Cantor in $\mathbb{R}$: a continuous real function on a compact subset of $\mathbb{R}$ is uniformly continuous, proved $\mathbb{R}$-natively from sequential compactness
- A continuous real function on a compact subset of $\mathbb{R}$ is bounded
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point
- Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $\mathbb{R}$, with the dictionary to monotone sequences
- Laws of finite sums and finite products
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
- W. Rudin, Principles of Mathematical Analysis, Ch. 6, Theorem 6.11 (standard reference, not scraped)