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
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.
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
(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.
(a) is INTEGRA4:29.
(b) is INTEGRA4:23 or INTEGRA6:7/8.
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
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.
No direct reference, but with continuity given by INTEGR19:55/56.
6.25 Theorem is INTEGR19:20/21.
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.
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.