# Rigorous computation of solutions of semi-linear PDEs on unbounded domains via spectral methods

## TL;DR

This paper introduces a rigorous, spectral, computer-assisted method using Fourier series and Newton-Kantorovich techniques to prove the existence of solutions to semi-linear PDEs on unbounded domains, including applications to solitons.

## Contribution

It develops a fully spectral, computer-assisted framework for proving existence of solutions to semi-linear PDEs on unbounded domains, extending to systems with parameters.

## Key findings

- Proved existence of a traveling wave (soliton) in the Kawahara equation.
- Constructed approximate inverses of differential operators via Fourier series.
- Established stability of the traveling wave solution.

## Abstract

In this article we present a general method to rigorously prove existence of strong solutions to a large class of autonomous semi-linear PDEs in a Hilbert space $H^{l}\subset H^{s}(\mathbb{R}^{m})$ ($s\geq1$) 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^{2}$ 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^{4}(\mathbb{R})$ as well as eigenpairs of the linearization about the soliton. These results allow us to prove the stability of the aforementioned traveling wave.