数值计算与严格数学

本书的作者现已退休。任何有能力的爱好者都欢迎进一步推动这个项目。

介绍

众所周知，数学通常证明永不相互矛盾的通用定理，而数值计算通常给出近似的特定结果；此类计算在合理的误差范围内可能不一致。在数值上下文中，“数字”通常意味着一个有限小数（或二进制数），而在数学中，一个（实数）数字可能是 $1/3$ （有理数，循环小数），${\sqrt {2}}$ （无理代数数；它的十进制表示既不终止也不无限循环），$\pi$ （超越数，即非代数数），等等。

数值误差 的估计（和最小化）是 数值分析 的重要组成部分。在某些（相对简单的）情况下，可以获得保证的误差界限，并且有时是实用的，但有时远大于它们从上面界定的实际误差，有时难以找到。因此，获得一个只有对误差有模糊概念的近似结果并不少见。

看到纯数学和应用数学之间的这些区别，人们可能会怀疑，它们仍然是同一科学的两面，还是两门不同的科学。有些人甚至区分“理论数”、“实用数”和“计算机数”，并将诸如 $\pi$ 和 $e$ 之类的数学常数视为缺乏精确数值的符号计算元素。

引用

以下是 Е.М. Левич (E.M. Levich) 的书 “Математическая физика и компьютерная математика” (“Mathematical physics and computer mathematics”) 中的两段引言（翻译成英语）。可在网上获取 这里 和 这里。

"在物理学家眼中，数学是一座单一的大厦，不仅可以在其中证明理论命题，而且还可以使用计算机（如果需要）获得数值结果。
然而，现代数学并非铁板一块，它由几种类型的数学组成，这些数学不仅在目标上有所不同，而且在研究的主要对象上也有所不同：理论数学、实用数学和计算机数学。将这些类型联系在一起的是，在每种类型中，研究的主要对象都是所谓的“数字”。这个概念在不同类型的数学中的含义是不同的，因此它们在性质和适用范围上有所不同。
应该注意的是，在现代科学中，数字的概念不够严格，它被视为一种反映某些定量实体的单一概念。”（第 2 页）

"第二种方法是在某些初始条件下对微分方程进行数值求解，以便获得某些定量结果以供实验验证。在这种情况下，我们面临着上一段中描述的方法论困难。由于没有逻辑可能性来确定作为计算过程的结果而获得的有限数字集是否为任务的解，因此实际上我们没有可以与实验结果进行比较的东西。由此可见，如果要验证物理理论，就必须用计算机对微分方程或微分方程组进行数值求解，那么这种理论是无法用实验来验证的。”（第 34 页的最后一段）

超有限主义者讨论了与这些想法相关的模糊观点。

• 超有限主义 在维基百科。

---

2016 年，在一次类似的讨论中，本文的作者被要求严格地证明数字 $e^{10}$ （计算器给出了类似 22026.46579481 的东西，但这在严格证明中不是有效的论据）的前 10 位数字确实是 22026.465794；换句话说，证明以下内容。

定理。 $\quad 22026.465794\leq e^{10}<22026.465795\,.$

他接受了挑战并证明了这个定理。这绝不是学术意义上的原创研究；数学期刊会将其拒绝为使用众所周知方法获得的微不足道的结果。每个专业数学家都可以轻松做到这一点。但是，由于它对专家来说意义不大，它可以帮助学生摆脱一些可能的误解。

• 定理不一定是通用的；一个特定的数值事实可以是一个定理。
• 所有定理的集合是无限的（就像自然数的集合一样）；数学文献中提出了有限多个最著名的定理（其中大多数是通用的），其他的则没有（同样，现在提到了有限多个自然数，其他的则没有）。
• 众所周知的数学常数具有精确的数值；通常，它们的十进制数字不遵循任何已知模式，但仍然可以通过算法生成；此外，无限数字序列的每个有限部分的正确性都是一个定理（其证明也可以通过算法生成）。可能的算法很多，但是只要定理不互相矛盾（希望永远不会），每个数字的唯一性就会得到保证。

证明，分析部分

引理 1. 对于所有满足 $0\leq x\leq 1:$ 的 $x$，以下不等式成立：

$0\leq e^{x}-{\big (}1+x+{\tfrac {1}{2}}x^{2}{\big )}\leq {\tfrac {2}{9}}x^{3}.$

该证明使用了两个众所周知的幂级数

$1+x+x^{2}+x^{3}+\dots ={\frac {1}{1-x}}\quad$ 对于 $-1<x<1,$

$1+{\frac {x}{1!}}+{\frac {x^{2}}{2!}}+{\frac {x^{3}}{3!}}+\dots =e^{x}\quad$ 对于 $-\infty <x<\infty .$

引理 1 的证明。 首先，$e^{x}-{\big (}1+x+{\tfrac {1}{2}}x^{2}{\big )}={\tfrac {1}{3!}}x^{3}+{\tfrac {1}{4!}}x^{4}+\dots \geq 0.$ 其次，

${\tfrac {1}{3!}}x^{3}+{\tfrac {1}{4!}}x^{4}+\dots ={\tfrac {1}{6}}x^{3}{\big (}1+{\tfrac {1}{4}}x+{\tfrac {1}{4\cdot 5}}x^{2}+\dots {\big )}\leq {\tfrac {1}{6}}x^{3}{\big (}1+{\tfrac {1}{4}}+{\tfrac {1}{4^{2}}}+\dots {\big )}={\tfrac {1}{6}}x^{3}\cdot {\tfrac {1}{1-{\tfrac {1}{4}}}}={\tfrac {2}{9}}x^{3}.$$\Box$

证明，算术部分

引理 1 非常常见；一般性结论通过符号计算证明。因此，证明非常简洁。相反，该定理陈述了一个特定的数值事实，其证明的算术部分本质上是将数值计算转换为证明，这很不寻常。因此，这里需要一些预备知识和解释。

每个人都知道 2+2=4；但是，由于它不是公理，因此需要证明。首先，定义：2 = 1+1；  3 = 2+1；  4 = 3+1 。其次，证明：2+2 = 2+(1+1) = (2+1)+1 = 3+1 = 4。类似地，你可以证明 4+3=7 等等。此外，2×2 = (1+1)×2 = 1×2 + 1×2 = 2+2 = 4，等等。（如果你想更深入的 формализация，请尝试 皮亚诺公理。）

下一步：如何证明 23×6 = 138 ？首先，定义：23 = 2×10+3；  100 = 10×10；  138 = 1×100+3×10+8 。其次，证明：23×6 = (2×10+3)×6 = (2×10)×6 + 3×6 = (2×6)×10 + 3×6 = (10+2)×10 + (1×10+8) = 100+(2+1)×10+8 = 138。确实，一些步骤被省略了，但希望你能填补空白。顺便说一下，为什么 138 < 163 ？ 因为 138 < 138+2 = 140 < 160 < 160+3 = 163。或者，如果你愿意，138 < 138 + 25 = 163。

因此，“23×6<163” 是（一个例子）一个具有（至少一个）证明的数学命题；换句话说，它是一个定理。（参见 理论（数学逻辑）：“从公理中推出的任何句子...都被称为该理论的定理”；另见 形式证明。）显然，所有定理的集合是无限的。

我们看到，使用自然数进行的算术运算没有问题（这并不奇怪：它们是精确的，而不是近似的）；它们可以转换为定理和证明（而且，这种转换可以通过算法自动化）。同样的结论也适用于带有有限小数的算术运算（精确计算，没有 舍入误差）。例如，命题“2.3×0.6<1.63”很容易简化为“23×6<163”。

现在我们回到定理的证明。我们引入数字 $x={\frac {10}{2^{22}}}={\frac {5}{2^{21}}}$ 并将其夹在两个有限小数之间，如下所示。

引理 2.   $238\,418\,579\,101\,562\cdot 10^{-20}\leq x\leq 238\,418\,579\,101\,563\cdot 10^{-20}.$

这些大型数字突然出现，你感到困惑吗？如果你感到困惑，请打开以下旁白。

证明可能很棘手

“形式证明或推导是句子...的有限序列，每个句子都是公理、假设或从序列中的前一个句子推导出来的。序列中的最后一个句子是一个定理”（形式证明）。仅此而已——不多也不少。证明不需要遵循任何策略。它可能很棘手；这里有一些例子。

为了因式分解多项式 $x^{4}+1$，我们添加和减去 $2x^{2}$：  $x^{4}+1=x^{4}+2x^{2}+1-2x^{2}=(x^{2}+1)^{2}-({\sqrt {2}}x)^{2}=(x^{2}-{\sqrt {2}}x+1)((x^{2}+{\sqrt {2}}x+1).$ 为什么偏偏是 $2x^{2}$？ 可以给出解释，但这不是因式分解的一部分。

为了计算 高斯积分 $\textstyle \int _{-\infty }^{\infty }e^{-x^{2}}\,dx$，我们引入二重积分 $\textstyle \iint e^{-x^{2}-y^{2}}\,dx\,dy.$ 为什么？ 只是一个技巧。

为了得到斐波那契数的奇妙 公式，我们考虑满足相同递归关系的等比数列。

为了证明一个数列 $(a_{n})_{n}$ 的性质，我们经常引入它的生成函数 $\textstyle f(x)=\sum _{n}a_{n}x^{n}$（学生们经常会好奇$x$ 是什么）。

• 通常，任何定义明确的数学对象可以在证明的任何阶段被引入，这取决于作者的判断；作者无需为此道歉。解释（如果有的话）是证明的评论，而不是证明的一部分。在一个证明中可以引入多个对象。

---

引理 2 的证明。 我们记 $a=238\,418\,579\,101\,562$ 并将所需的不等式改写为： $\textstyle a\leq 10^{20}\cdot {\frac {5}{2^{21}}}\leq a+1;$   $\textstyle 2a\leq 5^{21}\leq 2(a+1);$   $\textstyle 0\leq 5^{21}-2a\leq 2.$   只需计算   $5^{21}-2a=476\,837\,158\,203\,125-2\cdot 238\,418\,579\,101\,562=1.$ $\Box$

引理 3。   $284\,217\,094\cdot 10^{-20}\leq {\tfrac {1}{2}}x^{2}\leq 284\,217\,095\cdot 10^{-20}.$

引理 3 的证明。 我们记 $a=284\,217\,094$ 并重新写出所需的不等式：$\textstyle a\leq 10^{20}\cdot {\frac {1}{2}}\cdot {\frac {5^{2}}{2^{42}}}\leq a+1;$   $\textstyle 2^{23}a\leq 5^{22}\leq 2^{23}(a+1);$   $\textstyle 0\leq 5^{22}-2^{23}a\leq 2^{23}.$   我们计算   $5^{22}-2^{23}a=2\,384\,185\,791\,015\,625-8\,388\,608\cdot 284\,217\,094=2\,550\,473,$ 因此不等式变为 $0\leq 2\,550\,473\leq 8\,388\,608.$ $\Box$

引理 4。   $301\cdot 10^{-20}\leq {\tfrac {2}{9}}x^{3}\leq 302\cdot 10^{-20}.$

证明。 我们记 $a=301$ 并重写需要的不等式：$\textstyle a\leq 10^{20}\cdot {\frac {2}{9}}\cdot {\frac {5^{3}}{2^{63}}}\leq a+1;$   $\textstyle 9\cdot 2^{42}a\leq 5^{23}\leq 9\cdot 2^{42}(a+1);$   $\textstyle 0\leq 5^{23}-9\cdot 2^{42}a\leq 9\cdot 2^{42}.$   我们计算   $5^{23}-9\cdot 2^{42}a=11\,920\,928\,955\,078\,125-39\,582\,418\,599\,936\cdot 301=6\,620\,956\,497\,389,$ 不等式变为 $0\leq 6\,620\,956\,497\,389\leq 39\,582\,418\,599\,936.$ $\Box$

命题。 $\textstyle 238\,418\,863\,318\,656\cdot 10^{-20}\leq e^{10/2^{22}}-1\leq 238\,418\,863\,318\,960\cdot 10^{-20}.$

证明。 由四个引理可得，因为 $\textstyle 238\,418\,579\,101\,562+284\,217\,094=238\,418\,863\,318\,656,$ 且 $\textstyle 238\,418\,579\,101\,563+284\,217\,095+302=238\,418\,863\,318\,960.$ $\Box$

定理的证明。 命题给出了

$\textstyle 1.000\,002\,384\,188\,633\,186\,56\leq e^{10/2^{22}}\leq 1.000\,002\,384\,188\,633\,189\,60.$

考虑到 $\textstyle {\big (}e^{10/2^{22}}{\big )}^{2}=e^{2\cdot 10/2^{22}}=e^{10/2^{21}}$，我们得到 $\textstyle 1.000\,002\,384\,188\,633\,186\,56^{2}\leq e^{10/2^{21}}\leq 1.000\,002\,384\,188\,633\,189\,60^{2}$，因此

$\textstyle 1.000\,004\,768\,382\,950\,728\,55\leq e^{10/2^{21}}\leq 1.000\,004\,768\,382\,950\,734\,64$

（因为 $\textstyle 10^{20}\cdot 100000476838295072855\leq 100000238418863318656^{2}$ 以及 $\textstyle 100000238418863318960^{2}\leq 10^{20}\cdot 100000476838295073464$）。类似地，我们得到

$\textstyle 1.000\,009\,536\,788\,638\,933\,06\leq e^{10/2^{20}}\leq 1.000\,009\,536\,788\,638\,945\,25$

$\textstyle 1.000\,019\,073\,668\,228\,203\,66\leq e^{10/2^{19}}\leq 1.000\,019\,073\,668\,228\,228\,05$

$\textstyle 1.000\,038\,147\,700\,261\,226\,99\leq e^{10/2^{18}}\leq 1.000\,038\,147\,700\,261\,275\,79$

$\textstyle 1.000\,076\,296\,855\,769\,489\,20\leq e^{10/2^{17}}\leq 1.000\,076\,296\,855\,769\,586\,81$

$\textstyle 1.000\,152\,599\,532\,749\,178\,71\leq e^{10/2^{16}}\leq 1.000\,152\,599\,532\,749\,373\,95$$\textstyle 1.000\,305\,222\,352\,115\,752\,68\leq e^{10/2^{15}}\leq 1.000\,305\,222\,352\,116\,143\,23$

$\textstyle 1.000\,610\,537\,864\,915\,736\,43\leq e^{10/2^{14}}\leq 1.000\,610\,537\,864\,916\,517\,78$

$\textstyle 1.001\,221\,448\,486\,315\,968\,72\leq e^{10/2^{13}}\leq 1.001\,221\,448\,486\,317\,532\,39$

$\textstyle 1.002\,444\,388\,909\,036\,661\,01\leq e^{10/2^{12}}\leq 1.002\,444\,388\,909\,039\,792\,18$

$\textstyle 1.004\,894\,752\,855\,211\,943\,45\leq e^{10/2^{11}}\leq 1.004\,894\,752\,855\,218\,221\,11$

$\textstyle 1.009\,813\,464\,315\,937\,492\,37\leq e^{10/2^{10}}\leq 1.009\,813\,464\,315\,950\,109\,15$

$\textstyle 1.019\,723\,232\,713\,755\,163\,25\leq e^{10/2^{9}}\leq 1.019\,723\,232\,713\,780\,644\,45$

$\textstyle 1.039\,835\,471\,336\,191\,268\,36\leq e^{10/2^{8}}\leq 1.039\,835\,471\,336\,243\,235\,91$

$\textstyle 1.081\,257\,807\,448\,959\,052\,87\leq e^{10/2^{7}}\leq 1.081\,257\,807\,449\,067\,128\,28$

$\textstyle 1.169\,118\,446\,169\,330\,211\,07\leq e^{10/2^{6}}\leq 1.169\,118\,446\,169\,563\,925\,85$

$\textstyle 1.366\,837\,941\,173\,389\,062\,48\leq e^{10/2^{5}}\leq 1.366\,837\,941\,173\,935\,543\,01$

$\textstyle 1.868\,245\,957\,431\,108\,979\,33\leq e^{10/2^{4}}\leq 1.868\,245\,957\,432\,602\,879\,98$

$\textstyle 3.490\,342\,957\,457\,681\,064\,50\leq e^{10/2^{3}}\leq 3.490\,342\,957\,463\,263\,012\,21$

$\textstyle 12.182\,493\,960\,674\,431\,609\,26\leq e^{10/2^{2}}\leq 12.182\,493\,960\,713\,397\,433\,03$

$\textstyle 148.413\,159\,101\,868\,999\,612\,94\leq e^{10/2}\leq 148.413\,159\,102\,818\,401\,438\,45$

$\textstyle 22\,026.465\,794\,596\,681\,083\,829\,69\leq e^{10}\leq 22\,026.465\,794\,878\,488\,532\,192\,65$

完成了证明。 $\Box$

问题、练习、习题

在给定的证明中，引入了许多大型自然数，但没有解释。这些数字的属性似乎足以证明定理。

1a. 思考如何选择这些数字（不一定与本文中使用的数字相同）。

1b. 对计算机进行编程，以查找这些数字。

请注意，证明中的数字 22 是特殊的；最初，数字 $e^{10/2^{22}}$ 被夹在两个有限小数之间，然后对它进行 22 次平方运算。

2a. 思考一下，可以用 21 或 23 代替 22 吗？

2b. 修改您的计算机程序，使其进行 21 或 23 次平方运算。您仍然可以达到目标（证明定理）吗？另外，尝试更改大自然数中的位数。

2c. 考虑 $e^{x}$ 的其他值 $x$（不仅仅是 $x=10$）。

引理 1 中使用了二次多项式来近似指数函数。为什么只使用二次多项式？

3a. 思考一下，可以用线性或三次多项式代替吗？

3b. 相应地修改您的计算机程序。

3c. 尝试使用幂级数来摆脱重复平方运算。

计算指数函数，与微分方程 $\textstyle {\frac {dy}{dx}}=y,$ 密切相关，仅仅是一个相对简单的计算任务。

4a$^{*}$ 以同样的精神处理其他一些计算任务。

4b$^{**}$ 尝试找到一个计算任务的例子，即使在原则上也不能以这种方式处理。

以及一个奖励...

5$^{*}$ 证明 $\pi <{\frac {14-{\sqrt {2}}}{4}},$ 因此驳斥了 Sarva Jagannadha Reddy 关于 $\pi ={\frac {14-{\sqrt {2}}}{4}}$ 的说法（参见 这里 和 这里）。

结论

非严格的数值计算被广泛使用；严格的数值计算很费力，但也是可能的。

链接

• Warwick Tucker, Validated Numerics: A Short Introduction to Rigorous Computations，普林斯顿大学出版社，2011 年，152 页。
• 可靠计算，一本致力于保证精度的数学计算、范围界定、基于浮点运算的数学证明以及区间算术和其他理论的应用的开放式电子期刊。
• Fredrik Johansson, 严格计算超几何函数，电子预印本，2016 年。
• 验证数值，维基百科文章。
  • 计算机辅助证明，维基百科文章。
  • 区间算术，维基百科文章（验证数值的基本技术）。
  • 仿射算术，维基百科文章（区间算术的改进）。
  • INTLAB，用于可靠计算的 Matlab/Octave 工具箱。