Walter Rudin 的数学分析原理/微分 - Mizar 评论

实函数的导数

5.1 定义
Mizar 并没有像 Rudin 那样通过 $\phi (t)$ 来引入微分，而是直接使用线性函数和剩余函数（见FDIFF_1:def 2/3）。并没有参考将 Mizar 微分与LIMFUNC3的符号相关联，但有FDIFF_1:12和FDIFF_2:49。（顺便说一下，Mizar 微分并不局限于区间 $[a,b]$。）
$f$ 在 $x$ 处可微意味着f 在 x 处可微 (FDIFF_1:def 4), $f'(x)$ 是diff(f,x) (FDIFF_1:def 5）。$f$ 在 $E$ 上可微意味着f 在 E 上可微 (FDIFF_1:def 6), $f'$ 是f`|E (FDIFF_1:def 7）。另见FDIFF_1:def 8和POLYDIFF:def 1.
单侧微分在FDIFF_3.

5.2 定理 是FDIFF_1:24/25

5.3 定理
(a) 是FDIFF_1:13/18或POLYDIFF:14.
(b) 是FDIFF_1:16/21或POLYDIFF:16.
(c) 是FDIFF_2:14/21.

5.4 例子
对于常数 $c$，$c'=0$ 是FDIFF_1:11/22，另见POLYDIFF:11.
$x'=1$ 是FDIFF_1:17，另见POLYDIFF:12，更一般的 $(ax+b)'=a$ 是FDIFF_1:23.
多项式的微分由POLYDIFF:def 5/6和POLYDIFF:61给出。符号看起来有点复杂，因为多项式在 Mizar 中有相当多的结构，见PRE_POLY和POLYNOM系列。

5.5 定理 是FDIFF_2:23.

5.6 例子
(a) 是FDIFF_5:7.
(b) 是FDIFF_5:17，虽然 $f'(0)$ 被明确排除，没有参考。

中值定理

5.7 定义 没有参考。

5.8 定理 没有参考，虽然该陈述基本上在ROLLE:1的证明中得到了证明。#TODO 可微函数的局部极值有导数 0 的明确参考。

5.9 定理 是ROLLE:5.

5.10 定理 是ROLLE:3.

5.11 定理
(a) 是ROLLE:11或FDIFF_2:31.
(b) 是ROLLE:7.
(c) 是ROLLE:12或FDIFF_2:32.

导数的连续性

5.12 定理 无引用。 #TODO $f'(a)<\lambda <f'(b)$ 意味着存在一个 $x$ 使得 $f'(x)=\lambda$.

推论 无引用。

洛必达法则

5.13 定理 在L_HOSPIT中，尤其是L_HOSPIT:10.

高阶导数

5.14 定义
$f^{(n)}$ 是diff(f,E).n (TAYLOR_1:def 5，另见TAYLOR_1:def 6，其中 $E$ 是 $f^{(n)}$ 定义的域。

泰勒定理

5.15 定理
令 $c=\alpha$ 且 $d=\beta$，则 $P(t)$ 是Partial_Sums(Taylor(f,E,c,d)).(n-'1)（参见SERIES_1:def 1和TAYLOR_1:def 7），其中 $E$ 是 $f^{(n)}$ 定义的域。该定理是TAYLOR_1:27，其中用 $n+1$ 代替了 $n$.

向量值函数的微分

5.16 备注（关于复值函数）
Mizar 中没有形式化实数子集到复数的函数的微分，但复微分的定义由CFDIFF_1:def 6-9和CFDIFF_1:def 12，另见CFDIFF_1:22给出。可微复函数的连续性由CFDIFF_1:34/35. 微分规则 $f+g$ 和 $fg$ 分别由下式给出CFDIFF_1:23/28, CFDIFF_1:26/31分别给出。 $f/g$ 没有参考。

5.16 备注（关于赋范空间）
在NDIFF_1中，微分定义在赋范线性空间之间（参见NDIFF_1:def 6-9），即定义域不需要是实数的子集。关于可微性当且仅当分量可微性没有参考。另请参见PDIFF_1.
可微性意味着连续性由下式给出NDIFF_1:44/45.
$f+g$ 由下式给出NDIFF_1:35/39. 关于内积没有参考。

5.16 备注（关于向量值函数）
定义参见NDIFF_3:def 3-7，另见NDIFF_3:13. 关于可微性当且仅当分量可微性没有参考。另请参见NDIFF_4.
可微性意味着连续性由下式给出NDIFF_3:22/23.
$f+g$ 由下式给出NDIFF_3:14/17. 关于内积没有参考。

5.17 例子 没有参考。 $e^{z}$ 在SIN_COS:def 14中定义， $e^{ix}$ 由下式给出SIN_COS:25.

5.18 例子 没有参考。

5.19 定理 没有参考。

习题

1. 是FDIFF_2:25.
2. 是FDIFF_2:37/38或FDIFF_2:45.
3. 没有参考。
4. 没有参考。
5. 没有参考。
6. 没有参考。
7. 参见L_HOSPIT:10.
8. 没有参考。
9. 没有参考。
10. 没有参考。
11. 没有参考。
12. 没有参考。
13. 没有参考。
14. 没有参考。
15. 没有参考。
16. 没有参考。
17. 没有参考。
18. 没有参考。
19. 没有参考。
20. 没有参考。
21. 没有参考。
22. 没有参考。
23. 没有参考。
24. 没有参考。
25. 没有参考。
26. 没有参考。#TODO 找到 $|f(x)|\leq A|f'(x)|$ 意味着 $f=0$ 的参考。
27. 没有参考。#TODO 找到初始值问题的参考。
28. 没有参考。#TODO 找到初始值问题的参考。
29. 没有参考。