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 IntegralEdit

6.1 Definition
A partition is described by a Division (INTEGRA1:def 2), leaving   out and changing   to  . The intervals can be accessed via divset(P,i) (INTEGRA1:def 4), therefore   is given by vol divset(P,i) (INTEGRA1:def 5).
  is upper_sum(f,P) (INTEGRA1:def 8),   is lower_sum(f,P) (INTEGRA1:def 9).
  is upper_integral(f) (INTEGRA1:def 14),   is lower_integral(f) (INTEGRA1:def 15).
  being integrable is in INTEGRA1:def 16 (see also INTEGRA5:def 1),   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   is bounded and integrable and   is continuous, then   is integrable.

Properties of the IntegralEdit

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   with  .
(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
  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 DifferentiationEdit

6.20 Theorem
INTEGRA6:28/29, but no reference for the continuity of   if   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 FunctionsEdit

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 CurvesEdit

6.26 Definition
More generally,   being a parametrized-curve is defined in TOPALG_6:def 4, no reference for closed curves there. For simple closed curves in   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  -curves using another approach.
No reference for   or rectifiable.

6.27 Theorem No reference.

ExercisesEdit

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.