本书利用交互式定理证明工具Coq，在朴素集合论和初等数论及代数知识形式化系统下，以华东师范大学数学系编著的《数学分析》为基本构架，实现一元微积分的机器证明系统，包括实数与函数、数列极限、函数极限、函数的连续性、导数和微分、微分中值定理、实数的完备性、不定积分、定积分以及两个重要极限等内容的形式化实现。在我们开发的系统中，全部定理无一例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地应用于拓扑学和代数学理论的形式化构建，实现读者跟随计算机学习、理解、构建乃至发展现代数学的尝试，进一步提高认识数学、感受数学和欣赏数学的素养。
为方便应用和完整起见,附录中给出了Morse？Kelley公理集合论以及Zorich的著名著作《数学分析》中实数公理化形式系统的结构化表述。
样章试读
目录
- 目录
基本符号汇集
第0章 预备知识 1
0.1 概述 1
0.1.1 证明辅助工具Coq 1
0.1.2 形式化数学 2
0.1.3 公理化集合论系统 3
0.1.4 分析基础 5
0.1.5 本书结构安排 7
0.2 基本Coq指令清单及逻辑预备知识 8
0.3 朴素集合论与函数的初等概念 12
0.4 自然数的定义与有限集的若干性质 19
第1章 实数集与函数 27
1.1 实数 27
1.1.1 实数及其性质 27
1.1.2 绝对值与不等式 30
1.2 数集·确界原理 37
1.2.1 区间与邻域 37
1.2.2 有界集·确界原理 39
1.3 具有某些特性的函数 41
1.3.1 有界函数 41
1.3.2 单调函数 42
1.3.3 奇函数和偶函数 43
1.3.4 周期函数 44
1.3.5 函数的四则运算 44
第2章 数列极限 48
2.1 数列极限概念 48
2.2 收敛数列的性质 50
2.3 数列极限存在的条件 65
第3章 函数极限 74
3.1 函数极限概念 74
3.1.1 x趋于∞时函数的极限 74
3.1.2 x趋于x？时函数的极限 75
3.2 函数极限的性质 77
3.3 函数极限存在的条件 85
3.4 无穷小量与无穷大量 98
3.4.1 无穷小量 98
3.4.2 无穷小量阶的比较 100
3.4.3 无穷大量 104
第4章 函数的连续性 107
4.1 连续性概念 107
4.1.1 函数在一点的连续性 107
4.1.2 间断点及其分类 108
4.1.3 区间上的连续函数 109
4.2 连续函数的性质 109
4.2.1 连续函数的局部性质 109
4.2.2 闭区间上连续函数的基本性质 114
4.2.3 反函数的连续性 129
4.2.4 一致连续性 137
第5章 导数和微分 143
5.1 导数的概念 143
5.1.1 导数的定义 143
5.1.2 导函数 148
5.1.3 导数的几何意义 149
5.2 求导法则 151
5.2.1 导数的四则运算 151
5.2.2 反函数的导数 160
5.2.3 复合函数的导数 165
5.3 高阶导数 175
5.4 微分 180
5.4.1 微分的概念 180
5.4.2 微分的运算法则 183
5.4.3 高阶微分 184
第6章 微分中值定理 187
6.1 拉格朗日定理和函数的单调性 187
6.1.1 罗尔定理与拉格朗日定理 187
6.1.2 单调函数 194
6.2 柯西中值定理和不定式极限 208
6.2.1 柯西中值定理 208
6.2.2 不定式极限 214
6.3 泰勒公式 226
6.3.1 带有佩亚诺型余项的泰勒公式 226
6.3.2 带有拉格朗日型余项的泰勒公式 237
6.4 函数的极值与最大(小)值 249
6.4.1 极值判别 249
6.4.2 最大值与最小值 256
6.5 函数的凸性与拐点 257
第7章 实数的完备性 267
7.1 关于实数集完备性的基本定理 267
7.1.1 区间套定理 267
7.1.2 聚点定理与有限覆盖定理 269
7.1.3 实数完备性基本定理之间的等价性 270
7.2 上极限和下极限 271
第8章 不定积分 274
8.1 不定积分概念与基本积分公式 274
8.1.1 原函数与不定积分 274
8.1.2 基本积分公式 276
8.2 换元积分法与分部积分法 277
8.2.1 换元积分法 277
8.2.2 分部积分法 282
第9章 定积分 283
9.1 定积分概念 283
9.1.1 问题提出 283
9.1.2 定积分的定义 283
9.2 牛顿？莱布尼茨公式 289
9.3 可积条件 291
9.3.1 可积的必要条件 291
9.3.2 可积的充要条件 296
9.3.3 可积函数类 298
9.4 定积分的性质 311
9.4.1 定积分的基本性质 311
9.4.2 积分中值定理 327
9.5 微积分学基本定理·定积分计算(续) 330
9.5.1 变限积分与原函数的存在性 331
9.5.2 换元积分法与分部积分法 355
9.6 可积性理论补叙 361
9.6.1 上和与下和的性质 363
9.6.2 可积的充要条件 368
第10章 两个重要极限 372
10.1 级数的基本概念及性质 372
10.2 * 382
10.3 * 387
第11章 结论与注记 396
附录一 Coq指令说明 404
A.1 Coq专用术语 404
A.2 Coq证明指令 405
A.3 集成策略 408
附录二 公理集合论与实数公理化的结构性呈现 409
附录三 关于朴素集合论形式化的一点注记 436
参考文献 442
索引 456
后记 462
表格目录
表0.1 书中涉及的常用Coq术语的基本含义 9
表0.2 书中涉及的常用Coq指令简表 10
表11.1 一元微积分形式化系统代码量统计 397
插图目录
图0.1 Kelley《一般拓扑学》的英文版和中文版封面 4
图0.2 Landau《分析基础》的德文？英文版和中文版封面 5
图0.3 Zorich《数学分析》的俄文版、英文版、中文版封面 7
图0.4 华东师范大学数学系《数学分析》的五个版本封面 8
图7.1 实数的定义与完备性总览图 270
图11.1 微积分形式化系统文件依赖关系 398
图11.2 牛顿？莱布尼茨公式的证明截图 399
图11.3 计算机软件著作权登记证书 399
图11.4 Lean验证数学定理输出的命题和概念网络 400
图11.5 Lean验证多项式Freiman？Ruzsa猜想输出的Blueprint图 401
京公网安备 11010102004214号