Computer assisted proof of branches of stationary and periodic solution, and Hopf bifurcations, for dissipative PDEs

Let $\rho=65/64$, let $\mathcal{C}$ be the space of functions

such that

Denote by $\mathcal{C}_{S}$ the subspace of $\mathcal{C}$ characterized by the symmetry $f(x)=f(\pi-x)$, that is the subspace of functions with $f_{2k}=0$ for all $k=1,2,\ldots$. For $u=(U,V)\in\mathcal{C}^{2}$ let $\|u\|=\|U\|+\|V\|$. Let $A_{b}:\mathcal{C}^{2}\to\mathcal{C}^{2}$ be defined by

Clearly, fixed points of $A_{b}$ are analytic stationary solutions of (1). Also note that $A_{b}(U,V)\in\mathcal{C}_{S}^{2}$ for all $(U,V)\in\mathcal{C}_{S}^{2}$.

To prove that $A_{b}$ admits a fixed point $(U_{b},V_{b})\in\mathcal{C}_{S}^{2}$ for each $b\in[0,11]$, and that the function $b\mapsto(U_{b},V_{b})$ is analytic, we write all the coefficients in the Fourier expansion of $(U_{b},V_{b})$ as Taylor polynomials in $b$:

where $b_{0},b_{1}$ and $L$ are as in Table 1. As a first step, we choose some Fourier-Taylor polynomial $\bar{u}=(\bar{U},\bar{V})\in\mathcal{C}_{S}^{2}$ that is an approximate fixed point of $A_{b}$, and some finite rank operator $M_{b}:\mathcal{C}^{2}\to\mathcal{C}_{S}^{2}$ such that ${\mathbb{I}}-M_{b}$ is an approximate inverse of ${\mathbb{I}}-DA_{b}(\bar{u})$. Then for $h\in\mathcal{C}^{2}$ we define

Clearly, if $h$ is a fixed point of $\mathcal{M}_{b}$, then $u=\bar{u}+\Lambda_{b}h$ is a fixed point of $A_{b}$ and, hence, $u$ solves (1). Given $r>0$ and $w\in\mathcal{C}^{2}$, let $B_{r}(w)=\{v\in\mathcal{C}^{2}\,:\,\|v-w\|<r\}$. We partition the interval $[0,11]$ into four subintervals. The center $b_{0}$ and width $b_{1}$ for each subinterval are shown in Table 1.

Then we prove the following lemma with the aid of a computer, see Section 3.

This lemma, together with the Contraction Mapping Theorem and the Implicit Function Theorem, implies Theorem 1.

The time period $T$ of a (non stationary) periodic solution varies with $b$. Instead of looking for $T$-periodic solutions of equation (1), we look for $2\pi$-periodic solutions of

where $\alpha=2\pi/T$ has to be determined. To simplify notation, a $2\pi$-periodic function will be identified with a function on the circle $\mathbb{R}/(2\pi\mathbb{Z})$.

Let $\rho=33/32$ and $\varrho=1+2^{-20}$, let

and let ${\mathcal{A}}$ be the space of functions

with

Given $f\in{\mathcal{A}}$, let

Let ${\mathcal{B}}$ be the space of functions

with $U_{k},V_{k}\in{\mathcal{A}}$ and

Given $(U,V)\in{\mathcal{B}}$, let

and define $(U_{\rm e},V_{\rm e})$ similarly. For $b$ near the bifurcation point $b_{0}$, we expect $U,V$ to be nearly time-independent. So in particular, $(U_{\rm o},V_{\rm o})$ is close to zero. This justifies the following scaling: for some $\beta>0$ define

Substituting into (1) yields the equation

where $s=\beta^{2}$ and

Let

Then, if

we have

and (1) is equivalent to

One of the features of the equation is that the time-translate of a solution is again a solution. We eliminate this symmetry by imposing the condition $u_{11}=0$. In addition, close to the Hopf bifurcation point, we normalize the odd part of $u$ by choosing $u_{(-1)1}=1$. This leads to the conditions

It is convenient to regard $s$ to be the independent parameter and express $\alpha$ and $b$ as a function of $s$. The functions $\alpha=\alpha(s)$ and $b=b(s)$ are determined by the condition that $u$ satisfies (14). Applying $A$ and $B$ to both sides of $u={\mathbb{F}}_{s}(u,v)$, and using the identities $A\partial_{xx}=-A$, $A\partial_{t}=B$, $B\partial_{xx}=-B$, $B\partial_{t}=-A$, we find that

To compute the derivatives of $\{{\mathbb{F}}_{s},{\mathbb{G}}_{s}\}$, assume that $u,v$ depend on a parameter, and denote by a dot the derivative with respect to this parameter. Define

Then the parameter-derivatives of ${\mathbb{F}}_{s}(u,v)$ and ${\mathbb{G}}_{s}(u,v),$ are given by

where

Away from the Hopf bifurcation point there is no need to normalize the odd part of $u$, so that $b$ can be a free parameter and then we choose $\beta=1$. In this case, imposing the condition $Aw=0$ we find that

and the parameter-derivatives of ${\mathbb{F}}_{1}(u,v)$ and ${\mathbb{G}}_{1}(u,v),$ are given by

To prove that (1) admits a periodic solution $(U_{b},V_{b})\in\mathcal{C}_{S}^{2}$ for each $b\in[b_{0},b_{1}]$, and that the function $b\mapsto(U_{b},V_{b})$ is analytic, we follow a procedure similar to the stationary case: we write all the coefficients in the Fourier expansion of $(u,v)$ as Taylor polynomials in $s$:

Let

so that periodic solutions of (1) correspond to fixed points of ${\mathbb{H}}_{s}$. Let ${\mathcal{B}}_{S}\displaystyle\mathrel{\mathop{=}^{\scriptscriptstyle\rm def}}\{(u,v)\in{\mathcal{B}}\,:\,u(x,t)=u(\pi-x,t)\,,v(x,t)=v(\pi-x,t)\}$, and note that ${\mathbb{H}}_{s}(u,v)\in{\mathcal{B}}_{S}$ for all $(u,v)\in{\mathcal{B}}_{S}$.

As a first step, we choose some Fourier-Taylor polynomial $\bar{w}=(\bar{u},\bar{v})\in{\mathcal{B}}_{S}$, that is an approximate fixed point of ${\mathbb{H}}_{s}$, and some finite rank operator $M=M(s)$ such that ${\mathbb{I}}-M$ is an approximate inverse of ${\mathbb{I}}-D{\mathbb{H}}_{s}(\bar{w})$ and $Mw\in{\mathcal{B}}_{S}$ for all $w\in{\mathcal{B}}_{S}$. Then for $h\in{\mathcal{B}}_{S}$ we define

Clearly, if $h$ is a fixed point of ${\mathcal{N}}_{s}$, then $u=\bar{u}+\Lambda h\in{\mathcal{B}}_{S}$ is a fixed point of ${\mathbb{H}}_{s}$ and, hence, $u$ solves (1). Given $r>0$ and $w\in{\mathcal{B}}_{S}$, let $B_{r}(w)=\{v\in{\mathcal{B}}_{S}\,:\,\|v-w\|<r\}$. Lemmas 2 and 3 are proved with the aid of a computer, see Section 3.

Let $I$ be the natural embedding of $\mathcal{C}^{2}_{S}$ into ${\mathcal{B}}_{S}$.

These lemmas, together with the Contraction Mapping Theorem, imply the following proposition, which in turn yields Theorem 2.

Finally, Theorem 3 follows from the following Lemma, also proved with computer assistance:

Consider the linear operators ${\mathcal{L}}_{\alpha,d,b}$ and ${\mathcal{L}}_{\alpha,d,b}^{\prime}$, with $\alpha,d,b\in\mathbb{R}$. Let $\tilde{u}={\mathcal{L}}_{\alpha,d,b}u$. Using (12) and the Cauchy-Schwarz inequality in $\mathbb{R}^{2}$ we have the estimate

Note that $C_{j,k}$ is a decreasing function of $j,k$ and can be used to estimate ${\mathcal{L}}_{\alpha,d,b}u$ when $u$ is the tail of a Fourier series.

For the operator ${\mathcal{L}}_{\alpha,d,b}^{\prime}$ we have

A bound analogous to (20) holds, with with

The methods used here can be considered perturbation theory: given an approximate solution, prove bounds that guarantee the existence of a true solution nearby. But the approximate solutions needed here are too complex to be described without the aid of a computer, and the number of estimates involved is far too large.

The first part (finding approximate solutions) is a strictly numerical computation. The rigorous part is still numerical, but instead of truncating series and ignoring rounding errors, it produces guaranteed enclosures at every step along the computation. This part of the proof is written in the programming language Ada [14]. The following is meant to be a rough guide for the reader who wishes to check the correctness of our programs. The complete details can be found in [15].

In the present context, a “bound” on a map $f:{\mathcal{X}}\to{\mathcal{Y}}$ is a function $F$ that assigns to a set $X\subset{\mathcal{X}}$ of a given type (Xtype) a set $Y\subset{\mathcal{Y}}$ of a given type (Ytype), in such a way that $y=f(x)$ belongs to $Y$ for all $x\in X$. In Ada, such a bound $F$ can be implemented by defining a procedure F(X :  in Xtype ;  Y :  out Ytype).

To represent balls in a real Banach algebra ${\mathcal{X}}$ with unit ${\bf 1}$ we use pairs S=(S.C,S.R), where S.C is a representable number (Rep) and S.R a nonnegative representable number (Radius). The corresponding ball in ${\mathcal{X}}$ is $\langle{\tt S},{\mathcal{X}}\rangle=\{x\in{\mathcal{X}}:\|x-({\tt S.C}){\bf 1}\|\leq{\tt S.R}\}$.

When ${\mathcal{X}}=\mathbb{R}$ the data type described above is called Ball. Our bounds on some standard functions involving the type Ball are defined in the packages Flts_Std_Balls. Other basic functions are covered in the packages Vectors and Matrices. Bounds of this type have been used in many computer-assisted proofs; so we focus here on the more problem-specific aspects of our programs.

The computation and validation of branches involves Taylor series in one variable, which are represented by the type Taylor1 with coefficients of type Ball. The definition of the type and its basic procedures are in the package Taylors1. Given a Radius $\rho$, consider the space $\mathbb{T}_{\rho}$ of all real analytic functions $g(t)=\sum_{n}g_{n}t^{n}$ on the interval $|t|<\rho$, obtained by completing the space of polynomials with respect to the norm $\|g\|_{\rho}=\sum_{n}|g_{n}|\rho^{n}$. Given a positive integer D, a Taylor1 is a triple P=(P.C,P.F,P.R), where P.F is a nonnegative integer, ${\tt P.R}=\rho$, and P.C is an array(0..D) of Ball. The corresponding set in $\langle{\tt Taylor1},\mathbb{T}_{\rho}\rangle$ is defined as

where $m=\min({\tt P.F},{\tt D}+1)$. For the operations that we need in our proof, this type of enclosure allows for simple and efficient bounds.

Consider now the space ${\mathcal{A}}$ for a fixed domain radius $\varrho>1$ of type Radius. Functions in ${\mathcal{A}}$ are represented by the type Fourier1 defined in the package HFouriers1, which accepts coefficients in some Banach algebra with unit ${\mathcal{X}}$. In our application the coefficients of Fourier1 are Taylor1. The type Fourier1 consists of a triple F=(F.C,F.E,F.Freq0), where F.C is an array(-K,0..K) of Ball, F.E is an array(-2*K..2*K) of Radius and F.Freq0 is a boolean flag that, when True, indicates that the object Fourier1 represents a constant function. The corresponding set $\langle{\tt F},{\mathcal{A}}\rangle$ is the set of all function $u=p+h\in{\mathcal{A}}$, where

with $\|h^{J}\|\leq{\tt F.E(J)}$, for all $J$. Note that high order errors for the even frequencies and odd frequencies are handled separately. For the operations that we need in our proof, this type of enclosure allows for simple and efficient bounds. In particular, note that the nonlinearity in (11) requires a nonstandard product, depending on the parameter $s$. The procedure Prod in the package HFouriers1 provides bounds for that product.

We note that Fourier1 (just like Taylor1) allows a generic type Scalar for its coefficients; and this Scalar can be again a Taylor (or Fourier) series. This feature makes it easy to represent Fourier series whose coefficients depend on parameters.

To represent the space ${\mathcal{B}}$ we use a package Fouriers1 which is very similar to the package HFouriers1, so that we do not provide a detailed description here. The main differences consist in having a standard product, and high order errors for the even frequencies and odd frequencies are handles together.

More precisely, the package Fouriers1 is instantiated with scalars of type Fouriers1 defined in HFouriers1, which in turn has scalars defined in Taylors1. For simplicity, the space $\mathcal{C}$ is represented with the same object, with $K=0$.

A bound on the map ${\mathbb{H}}_{s}$ is implemented by the procedure GMap in the package Taylors1.Foor.Fix. Defining and estimating a contraction like ${\mathcal{N}}_{\beta}$ is a common task in many of our computer-assisted proofs. An implementation is done via two generic packages, Linear and Linear.Contr. For a description of this process we refer to [17].