# 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

edit**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 Integral

edit**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 Differentiation

edit**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 Functions

edit**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

edit**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.

## Exercises

edit1. 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.