Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis/The Riemann-Stieltjes Integral

In Mizar the Riemann-Stieltjes integral wasn't formalized until recently, so this chapter will primarily deal with that variant. Everything about the Riemann-Stieltjes integral in Mizar at the time of writing is in INTEGR22 and INTEGR23.

Definition and Existence of the Integral

6.1 Definition
A partition is described by a Division (INTEGRA1:def 2), leaving $x_0$ out and changing $\le$ to $<$. The intervals can be accessed via divset(P,i) (INTEGRA1:def 4), therefore $\mathrm{\Delta }{x}_i$ is given by vol divset(P,i) (INTEGRA1:def 5).
$U(P,f)$ is upper_sum(f,P) (INTEGRA1:def 8), $L(P,f)$ is lower_sum(f,P) (INTEGRA1:def 9).
${\bar{\int }}_a^{b}fdx$ is upper_integral(f) (INTEGRA1:def 14), ${\underset{\_}{\int }}_a^{b}fdx$ is lower_integral(f) (INTEGRA1:def 15).
$f$ being integrable is in INTEGRA1:def 16 (see also INTEGRA5:def 1), ${\int }_a^{b}fdx$ is integral(f) (INTEGRA1:def 17, see also INTEGRA5:def 4 for explicit integration bounds and INTEGRA7:def 2 for indefinite integral).
The inequalities are given by INTEGRA1:25,28,27.

6.2 Definition in INTEGR22.

6.3 Definition
Refinement is INTEGRA1:def 18. No reference for definition of common refinement, but it is given by INTEGRA1:47 and more precise by INTEGRA3:21.

6.4 Theorem is INTEGRA1:41/40.

6.5 Theorem is INTEGRA1:49.

6.6 Theorem is implicitly given by INTEGRA4:12.

6.7 Theorem No reference.

6.8 Theorem is INTEGRA5:11, for Riemann-Stieltjes INTEGR23:21.

6.9 Theorem is INTEGRA5:16.

6.10 Theorem No reference.

6.11 Theorem No reference. #TODO Reference that if $f$ is bounded and integrable and $\varphi$ is continuous, then $\varphi \circ f$ is integrable.

Properties of the Integral

6.12 Theorem
(a) is INTEGRA1:57 or INTEGRA6:11 and INTEGRA2:31 or INTEGRA6:9.
(b) is INTEGRA2:34.
(c) is INTEGRA6:17. No reference for something like $\underset{A\cup B}{\int }fdx=\underset{A}{\int }fdx+\underset{B}{\int }fdx$ with $A\cap B=\mathrm{\varnothing }$.
(d) No direct reference, but 6.13(b) improves the bound anyway.
(d) No reference.

6.13 Theorem
(a) is INTEGRA4:29.
(b) is INTEGRA4:23 or INTEGRA6:7/8.

6.14 Definition
$I$ equals chi(REALPLUS,REAL) (FUNCT_3:def 3, MUSIC_S1:def 2).

6.15 Theorem No reference.

6.16 Theorem No reference.

6.17 Theorem No reference. #TODO Relation between the Riemann and the Riemann-Stieltjes integral.

6.18 Remark No reference.

6.19 Theorem (change of variable) No reference. #TODO Find reference!

Integration and Differentiation

6.20 Theorem
INTEGRA6:28/29, but no reference for the continuity of $F$ if $f$ is only integrable.

6.21 The fundamental theorem of calculus is INTEGRA7:10.

6.22 Theorem (integration by parts) is INTEGRA5:21 or INTEGRA7:21/22.

Integration of vector-valued Functions

6.23 Definition Given by INTEGR15:def 13/14 and INTEGR15:def 16-18. Theorem 6.12 (a) translates to INTEGR15:17/18. Theorem 6.12 (c) translates to INTEGR19:8. No reference for a translation of Theorem 6.12 (e) or Theorem 6.17, since we're still looking at Riemann integrals only.

6.24 Theorem
No direct reference, but with continuity given by INTEGR19:55/56.

6.25 Theorem is INTEGR19:20/21.

Rectifiable Curves

6.26 Definition
More generally, $\gamma$ being a parametrized-curve is defined in TOPALG_6:def 4, no reference for closed curves there. For simple closed curves in $R^2$ see the attribute being_simple_closed_curve (TOPREAL2:def 1). In pursuing the proof of the Jordan Curve Theorem a lot of articles have been written dealing with that attribute, in contrast to parametrized-curve. Also see INTEGR1C:def 3 for a formalization of ${𝒞}^1$-curves using another approach.
No reference for $\mathrm{\Lambda }(\gamma )$ or rectifiable.

6.27 Theorem No reference.

Exercises

1. No reference.
2. No reference.
3. No reference.
4. No reference.
5. No reference.
6. No reference.
7. No reference.
8. See INTEGR10 for the definitions. No reference for exercise.
9. No reference.
10. No reference.
11. No reference.
12. No reference.
13. No reference.
14. No reference.
15. No reference.
16. No reference.
17. No reference.
18. No reference.
19. No reference.