Mizar 对 Walter Rudin 的《数学分析原理》的评注/黎曼-斯蒂尔杰斯积分

在 Mizar 中，黎曼-斯蒂尔杰斯积分直到最近才被形式化，因此本章将主要讨论该变体。在撰写本文时，Mizar 中有关黎曼-斯蒂尔杰斯积分的所有内容都在INTEGR22以及INTEGR23.

积分的定义与存在性

6.1 定义
一个划分由一个分割 (INTEGRA1:def 2）来描述，它把 $x_{0}$ 去掉，并将 $\leq$ 变成 $<$。可以通过以下方式访问这些区间divset(P,i) (INTEGRA1:def 4），因此 $\Delta x_{i}$ 由以下给出vol divset(P,i) (INTEGRA1:def 5).
$U(P,f)$ 是upper_sum(f,P) (INTEGRA1:def 8），$L(P,f)$ 是lower_sum(f,P) (INTEGRA1:def 9).
$\textstyle {\overline {\int }}_{a}^{b}f\,dx$ 是upper_integral(f) (INTEGRA1:def 14），$\textstyle {\underline {\int }}_{a}^{b}f\,dx$ 是lower_integral(f) (INTEGRA1:def 15).
$f$ 是可积的在INTEGRA1:def 16（另见INTEGRA5:def 1），$\textstyle {\int }_{a}^{b}f\,dx$ 是integral(f) (INTEGRA1:def 17，另见INTEGRA5:def 4以获取显式积分边界，以及INTEGRA7:def 2以获取不定积分）。
不等式由以下给出INTEGRA1:25,28,27.

6.2 定义 在INTEGR22.

6.3 定义
细化是INTEGRA1:def 18。没有关于公共细化定义的参考，但它由以下给出INTEGRA1:47并由以下更精确地给出INTEGRA3:21.

6.4 定理 是INTEGRA1:41/40.

6.5 定理 是INTEGRA1:49.

6.6 定理 由以下隐式给出INTEGRA4:12.

6.7 定理 没有参考。

6.8 定理 是INTEGRA5:11，对于黎曼-斯蒂尔杰斯INTEGR23:21.

6.9 定理 是INTEGRA5:16.

6.10 定理 没有参考。

6.11 定理 未找到引用。#TODO 引用如果 $f$ 有界且可积，而 $\phi$ 是连续的，那么 $\phi \circ f$ 是可积的。

积分的性质

6.12 定理
(a) 是INTEGRA1:57或INTEGRA6:11以及INTEGRA2:31或INTEGRA6:9.
(b) 是INTEGRA2:34.
(c) 是INTEGRA6:17. 未找到类似 $\textstyle \int _{A\cup B}f\,dx=\int _{A}f\,dx+\int _{B}f\,dx$ 其中 $A\cap B=\emptyset$ 的引用。
(d) 没有直接引用，但 6.13(b) 改善了界限。
(d) 未找到引用。

6.13 定理
(a) 是INTEGRA4:29.
(b) 是INTEGRA4:23或INTEGRA6:7/8.

6.14 定义
$I$ 等于chi(REALPLUS,REAL) (FUNCT_3:def 3, MUSIC_S1:def 2).

6.15 定理 未找到引用。

6.16 定理 未找到引用。

6.17 定理 未找到引用。#TODO 黎曼积分和黎曼-斯蒂尔切斯积分之间的关系。

6.18 备注 未找到引用。

6.19 定理（变量替换） 未找到引用。#TODO 查找引用！

积分与微分

6.20 定理
INTEGRA6:28/29, 但未找到 $F$ 连续性的引用，如果 $f$ 仅可积。

6.21 微积分基本定理 是INTEGRA7:10.

6.22 定理（分部积分） 是INTEGRA5:21或INTEGRA7:21/22.

向量值函数的积分

6.23 定义 由INTEGR15:def 13/14以及INTEGR15:def 16-18. 定理 6.12 (a) 转换为INTEGR15:17/18. 定理 6.12 (c) 转换为INTEGR19:8. 未找到定理 6.12 (e) 或定理 6.17 的转换引用，因为我们仍在研究黎曼积分。

6.24 定理
没有直接引用，但连续性由INTEGR19:55/56.

6.25 定理 是INTEGR19:20/21.

可求长曲线

6.26 定义
更一般地，$\gamma$ 是一个参数曲线在TOPALG_6:def 4中定义，没有找到封闭曲线的引用。对于 $R^{2}$ 中的简单封闭曲线，请参阅属性being_simple_closed_curve (TOPREAL2:def 1）。在追求证明 Jordan 曲线定理的过程中，已经发表了大量关于该属性的文章，这与参数曲线形成对比。另请参阅INTEGR1C:def 3，了解使用另一种方法对 ${\mathcal {C}}^{1}$ 曲线的形式化。
未找到 $\Lambda (\gamma )$ 或 可求长 的引用。

6.27 定理 未找到引用。

练习

1. 未找到引用。
2. 未找到引用。
3. 未找到引用。
4. 未找到引用。
5. 未找到引用。
6. 未找到引用。
7. 未找到引用。
8. 参阅INTEGR10了解定义。没有找到练习的引用。
9. 未找到引用。
10. 未找到引用。
11. 未找到引用。
12. 未找到引用。
13. 未找到引用。
14. 未找到引用。
15. 未找到引用。
16. 未找到引用。
17. 无参考。
18. 无参考。
19. 无参考。