Hans Koch, Alain Schenkel, and Peter Wittwer, "Computer-assisted proofs in analysis and programming in logic", SIAM Reviews, 1996 (to appear; the paper is stored in the mathematical physics archive, , paper 94-394).

This paper explains interval methods in Banach spaces to prove the existence of solutions for functional equations.

As a case study, the authors consider the Feigenbaum equation $\varphi(x)=\lambda^{-1}\varphi(\varphi(\lambda x))$ that stems from dynamical systems theory. A dynamical system with discrete time is an operator $T:X\to X$ that describes how a state $x(t)\in X$ at a moment of time $t$ is transformed into the state $x(t+1)=T(x(t))$ at the next moment of time. For an arbitrary $n$, we have $x(t+n)=T^n(x(t))$. How can we describe the asymptotic behavior of a generic 1-D dynamical system (i.e., of a dynamical system in which a state space $X$ is a real line)? The very term "asymptotic behavior" means that for all sufficiently large $n$, the transformations $T^n$ are similar. In particular, for large $n$, the transformations $T^n(x)$ and $T^{2n}(x)=T^n(T^n(x))$ must be similar. By {\it similar}, we mean that these operations may be mathematically different, but they are physically equivalent in the following sense: if we appropriately change the unit in which we measure $x$ (to a new one that is $\lambda$ times smaller for some $\lambda>0$), i.e., if we use $x'=\lambda\cdot x$ instead of $x$, then the expression for $T^{2n}$ in the new units will be almost identical to the expression for $T^{n}$ in the old ones (and the larger the $n$, the closer this similarity will be). In other words, if $y=T^n(x)$, then $y'\approx T^{2n}(x')$, where $y'=\lambda\cdot y$ and $x'=\lambda\cdot x$. In other words, $\lambda T^n(x)\approx T^n(T^n(\lambda x))$. When $n\to\infty$, then for the limit transformation $T^n\to\varphi$, we get the Feigenbaum equation $\lambda \varphi(x)=\varphi(\varphi(\lambda x))$.

The Feigenbaum equation was derived for 1-D systems, but it appears in multi-dimensional systems as well.

The existence of a solution to this equation is usually proved by showing that this equation describes a fixed point of a contraction mapping in Banach space (i.e., a mapping $m$ for which $\|m(x)-m(y)\|\le\beta\|x-y\|$ for some $\beta<1$). To check that the corresponding mapping is a contraction, the authors use "intervals" in Banach space, i.e., balls with a polynomial as a center and a given radius.

The proof itself is not new, but it is a good illustration of general interval techniques.

The paper also proposes a solution to the problem of publishing such proofs in an understandable way: to write a proof in Prolog, the language of logic programming. Also, this paper gives an introduction to Prolog, so that even a reader without previous exposure to programming should be able to verify the correctness of the proof.

In addition, this paper contains an exhaustive list of references to computer assisted proofs in analysis.

Edited from the author's abstract and an abstract by P. Wittwer.