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. 無參考。