Rigorous Computation of Solutions of Semilinear PDEs on Unbounded Domains via Spectral Methods

In this article we present a general method to rigorously prove existence of strong solutions to a large class of autonomous semilinear PDEs in a Hilbert space H^l \subset H^s(\BbbR^m) (s \geq 1) via computer-assisted proofs. Our approach is fully spectral and uses Fourier series to approximate functions in H^l as well as bounded linear operators from L² to H^l. In particular, we construct approximate inverses of differential operators via Fourier series approximations. Combining this construction with a Newton-Kantorovich approach, we develop a numerical method to prove existence of strong solutions. To do so, we introduce a finite-dimensional trace theorem from which we build smooth functions with support on a hypercube. The method is then generalized to systems of PDEs with extra equations/parameters, such as eigenvalue problems. As an application, we prove the existence of a traveling wave (soliton) in the Kawahara equation in H⁴(\BbbR) as well as eigenpairs of the linearization about the soliton. These results allow us to prove the stability of the aforementioned traveling wave.