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