Monotonicity, additivity and bounds for the Riemann-Stieltjes integral (Rudin 6.12 b,c,d), corrected

Basic properties of the Riemann–Stieltjes integral. Let $\alpha$ be monotonically increasing on $[a,b]$ and let $f, g \in \mathcal{R}(\alpha)$ on $[a,b]$, both bounded. Then:

1. (Monotonicity.) If $f(x) \le g(x)$ on $[a,b]$, then $\displaystyle\int_a^b f\,d\alpha \le \int_a^b g\,d\alpha$.
2. (Additivity over adjacent intervals.) For every $c \in [a,b]$, $f \in \mathcal{R}(\alpha)$ on $[a,c]$ and on $[c,b]$, and

3. (Bound.) If $|f(x)| \le M$ on $[a,b]$, then $\left|\int_a^b f\,d\alpha\right| \le M\,(\alpha(b) - \alpha(a))$.

These are parts (b), (c) and (d) of Rudin's Theorem 6.12.

Formalization note. Boundedness is part of Rudin's standing setup in Chapter 6 — his $\mathcal{R}(\alpha)$ consists of bounded functions — and it must be stated explicitly here. Upper and lower sums are built from sSup and sInf, which return the junk value $0$ on sets that are unbounded, so an unbounded function can satisfy the formal integrability predicate with integral $0$. On $[0,1]$ with $\alpha = \mathrm{id}$, take $f(0) = -1$ and $f(x) = -1/x$ for $x \neq 0$: every upper sum set is unbounded below and every lower sum is $\le 0$ with the value $0$ attained at the trivial partition, so both the upper and the lower integral come out $0$. With $g \equiv -1$ one has $f \le g$ on $[0,1]$ while part 1 would demand $0 \le -1$. The two boundedness hypotheses match those already carried by Rudin.ch06_linearity.