Numerical calculations and rigorous mathematics

The originator of this book is now retired. Any competent enthusiast is welcome to further this project.

Introduction

Everyone knows that mathematics usually proves general theorems that never contradict one another, while numerical calculations usually give particular results approximately; such calculations may disagree within a reasonable error. In the numerical context "number" usually means a terminating decimal (or binary), while in mathematics a (real) number may be $1/3$ (rational number, repeating decimal), ${\sqrt {2}}$ (irrational algebraic number; its decimal representation neither terminates nor infinitely repeats), $\pi$ (transcendent, that is, not algebraic), etc.

Estimation (and minimization) of numerical errors is an important part of numerical analysis. Guaranteed error bounds are available in some (relatively simple) cases, and are sometimes practical, but sometimes much greater than the actual errors they bound from above, and sometimes prohibitively laborious to find. Thus it is not uncommon to get an approximate result having only a vague idea about its error.

Being impressed by these distinctions between pure mathematics and applied mathematics one may wonder, are they still two sides of one science, or two different sciences. Some go so far as to distinguish between "theoretical numbers", "pragmatic numbers" and "computer numbers" and consider mathematical constants like $\pi$ and $e$ as elements of symbolic calculations devoid of exact numerical values.

quotes

Here are two quotes (translated into English) from the book by Е.М. Левич (E.M. Levich), "Математическая физика и компьютерная математика" ("Mathematical physics and computer mathematics"), in Russian. Available online here and here.

"In the eyes of physicists, mathematics is a single building, in which not only one can prove theoretical statements, but also obtain numerical results, using computers, if necessary.
However, modern mathematics is not a monolith, it consists of several types of mathematics that differ from each other not only by their goals, but also by the main objects of research: theoretical mathematics, pragmatical mathematics and computer mathematics. Uniting these types is the fact that in each of them the main objects of research are the so-called "numbers". The meaning of this concept in different types of mathematics is different, so they differ from each other in their properties and areas of applicability.
It should be noted that in modern science the concept of numbers is not strict enough, it is treated as a kind of single concept that reflects certain quantitative entities." (page 2)

"The second way consists in the numerical solution of the differential equations for certain initial conditions in order to obtain certain quantitative results for verification by experiment. In this case, we are faced with methodological difficulties described in the previous paragraph. Because there is no logical possibility to determine whether the finite set of numbers obtained as a result of the computational process is the solution of the task, we do not have, in fact, what to compare with the experimental results. From what has been said, it follows that if to check the physical theory is necessary to solve numerically by a computer a differential equation or a system of differential equations, then such a theory is unverifiable by experiment." (the last paragraph, page 34)

Vaguely related ideas are discussed by ultrafinitists.

• Ultrafinitism at Wikipedia.

---

Once in 2016, during a discussion of this kind, the originator of this essay was challenged to prove rigorously that the first 10 digits of the number $e^{10}$ (a calculator gives something like 22026.46579481 but is not a valid argument in rigorous proof) are indeed 22026.465794; in other words, to prove the following.

Theorem. $\quad 22026.465794\leq e^{10}<22026.465795\,.$

He accepted the challenge and proved this theorem. It is in no way an original research in the academic sense; a mathematical journal would reject it as a trivial result obtained by straightforward use of well-known methods. Every professional mathematician can do it easily. But, being of little interest to experts, it can help a student to get rid of some possible misconceptions.

• A theorem is not necessarily general; a particular numerical fact can be a theorem.
• The set of all theorems is infinite (just as the set of natural numbers); finitely many most notable theorems are presented in mathematical literature (and most of them are general), others are not (and similarly, finitely many natural numbers are mentioned for now, others are not).
• Well-known mathematical constants have exact numerical values; usually, their decimal digits do not follow any known pattern, but still can be generated by an algorithm; moreover, correctness of every finite portion of the infinite sequence of digits is a theorem (whose proof also can be generated by an algorithm). Possible algorithms are numerous, but uniqueness of every digit is guaranteed as long as theorems do not contradict one another (hopefully, forever).

The proof, analytic part

Lemma 1. The following inequality holds for all $x$ such that $0\leq x\leq 1:$

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

The proof uses two well-known power series

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

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

Proof of Lemma 1. First, $e^{x}-{\big (}1+x+{\tfrac {1}{2}}x^{2}{\big )}={\tfrac {1}{3!}}x^{3}+{\tfrac {1}{4!}}x^{4}+\dots \geq 0.$ Second,

${\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$

The proof, arithmetic part

Lemma 1 is quite usual; a general fact is proved by symbolic calculations. Accordingly, the proof is concise. In contrast, the theorem states a particular numerical fact, and the arithmetic part of its proof is basically a numeric calculation converted into a proof, which is unusual. Accordingly, some preliminaries and explanations are needed here.

Everyone known that 2+2=4; but, being not an axiom, this fact needs a proof. First, definitions: 2 = 1+1;   3 = 2+1;   4 = 3+1 . Second, the proof: 2+2 = 2+(1+1) = (2+1)+1 = 3+1 = 4. Similarly you can prove that 4+3=7 etc. Also, 2×2 = (1+1)×2 = 1×2 + 1×2 = 2+2 = 4, etc. (If you wish even deeper formalization, try Peano axioms.)

Next step: how to prove that 23×6 = 138 ? First, definitions: 23 = 2×10+3;   100 = 10×10;   138 = 1×100+3×10+8 . Second, the proof: 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. True, some steps are skipped, but hopefully you can fill in the gaps. And by the way, why 138 < 163 ? Since 138 < 138+2 = 140 < 160 < 160+3 = 163. Or, if you prefer, 138 < 138 + 25 = 163.

Thus, "23×6<163" is (an example of) a mathematical statement that has (at least one) proof; in other words, it is a theorem. (See Theory (mathematical logic): "any sentence that follows from the axioms ... is called a theorem of the theory"; see also Formal proof.) Clearly, the set of all theorems is infinite.

We see that arithmetic calculations with natural numbers are unproblematic (and no wonder: they are exact, not approximate); they can be converted to theorems and proofs (and moreover, such conversion can be automated by an algorithm). The same holds for arithmetic calculations with terminating decimals (exact calculations, with no round-off errors). For instance, the statement "2.3×0.6<1.63" reduces readily to "23×6<163".

Now we return to the proof of the theorem. We introduce the number $x={\frac {10}{2^{22}}}={\frac {5}{2^{21}}}$ and squeeze it between two terminating decimals as follows.

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

Are you disturbed by the sudden unexplained emergence of these large numbers? If you are, open the following digression.

A proof may be tricky

"A formal proof or derivation is a finite sequence of sentences ..., each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem" (Formal proof). Just that - no more, no less. The proof is not required to follow any strategy. It may be tricky; here are some examples.

In order to factor the polynomial $x^{4}+1$ one adds and subtracts $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).$ Why just $2x^{2}$? An explanation can be given, but is not a part of the factorization.

In order to calculate the Gaussian integral $\textstyle \int _{-\infty }^{\infty }e^{-x^{2}}\,dx$ one introduces the double integral $\textstyle \iint e^{-x^{2}-y^{2}}\,dx\,dy.$ Why? Just a trick.

In order to get the wonderful formula for Fibonacci numbers one considers geometric progressions satisfying the same recurrence relation.

In order to prove a property of a sequence $(a_{n})_{n}$ one often introduces its generating function $\textstyle f(x)=\sum _{n}a_{n}x^{n}$ (and students often wonder what $x$ is).

• Generally, any well-defined mathematical object may be introduced at any stage of a proof, at the author's discretion; no apology is expected from the author. Explanations (if any) are comments to the proof, not a part of the proof. Several objects may be introduced during one proof.

---

Proof of Lemma 2. We denote $a=238\,418\,579\,101\,562$ and rewrite the needed inequality: $\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.$   It remains to calculate   $5^{21}-2a=476\,837\,158\,203\,125-2\cdot 238\,418\,579\,101\,562=1.$ $\Box$

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

Proof of Lemma 3. We denote $a=284\,217\,094$ and rewrite the needed inequality: $\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}.$   We calculate   $5^{22}-2^{23}a=2\,384\,185\,791\,015\,625-8\,388\,608\cdot 284\,217\,094=2\,550\,473,$ and the inequality becomes $0\leq 2\,550\,473\leq 8\,388\,608.$ $\Box$

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

Proof. We denote $a=301$ and rewrite the needed inequality: $\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}.$   We calculate   $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,$ and the inequality becomes $0\leq 6\,620\,956\,497\,389\leq 39\,582\,418\,599\,936.$ $\Box$

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

Proof. Follows from the four lemmas, since $\textstyle 238\,418\,579\,101\,562+284\,217\,094=238\,418\,863\,318\,656,$ and $\textstyle 238\,418\,579\,101\,563+284\,217\,095+302=238\,418\,863\,318\,960.$ $\Box$

Proof of Theorem. Proposition gives

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

Taking into account that $\textstyle {\big (}e^{10/2^{22}}{\big )}^{2}=e^{2\cdot 10/2^{22}}=e^{10/2^{21}}$ we get $\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}$ whence

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

(since $\textstyle 10^{20}\cdot 100000476838295072855\leq 100000238418863318656^{2}$ and $\textstyle 100000238418863318960^{2}\leq 10^{20}\cdot 100000476838295073464$). Similarly we get

$\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$

which completes the proof. $\Box$

Questions, exercises, problems

A lot of large natural numbers are introduced in the given proof with no explanation. It appears that properties of these numbers are sufficient for proving the theorem.

1a. Think, how to choose such numbers (not necessarily equal to these used in this essay).

1b. Program the computer to find such numbers.

Note that the number 22 is special in the proof; initially, the number $e^{10/2^{22}}$ is squeezed between two terminating decimals, and then squaring is applied 22 times.

2a. Think, can 21 or 23 be used in place of 22?

2b. Modify your computer program in order to square 21 or 23 times. Do you still reach the goal (to prove the theorem)? Also try to change the number of digits in the large natural numbers.

2c. Consider $e^{x}$ for other values of $x$ (not just $x=10$).

Quadratic polynomial is used in Lemma 1 as an approximation of the exponential function. Why just quadratic?

3a. Think, can a linear or cubic polynomial be used instead?

3b. Modify your computer program accordingly.

3c. Try to use the power series in order to get rid of the repeated squaring.

Calculation of the exponential function, closely related to the differential equation $\textstyle {\frac {dy}{dx}}=y,$ is just one, relatively simple computational task.

4a$^{*}$ Treat some other computational tasks in the same spirit.

4b$^{**}$ Try to find an example of a computational task that cannot be treated this way, even in principle.

And a bonus...

5$^{*}$ Prove that $\pi <{\frac {14-{\sqrt {2}}}{4}},$ thus disproving a claim of Sarva Jagannadha Reddy that $\pi ={\frac {14-{\sqrt {2}}}{4}}$ (see here and here).

Conclusion

Non-rigorous numerical calculations are widely used; rigorous numerical calculations are laborious but possible.

Links

• Warwick Tucker, Validated Numerics: A Short Introduction to Rigorous Computations, Princeton University Press, 2011, 152 pages.
• Reliable Computing, An open electronic journal devoted to mathematical computations with guaranteed accuracy, bounding of ranges, mathematical proofs based on floating point arithmetic, and other theory and applications of interval arithmetic and directed rounding.
• Fredrik Johansson, Computing hypergeometric functions rigorously, e-print, 2016.
• Validated numerics, a Wikipedia article.
  • Computer-assisted proof, a Wikipedia article.
  • Interval arithmetic, a Wikipedia article (basic technique for validated numerics).
  • Affine arithmetic, a Wikipedia article (improvement of interval arithmetic).
  • INTLAB, The Matlab/Octave toolbox for Reliable Computing.