Computer-assisted Existence Proofs for Navier-Stokes Equations on an Unbounded Strip with Obstacle

The incompressible stationary 2D Navier-Stokes equations are considered on an unbounded strip domain with a compact obstacle. First, a computer-assisted existence and enclosure result for the velocity (in a suitable divergence-free Sobolev space) is presented. Starting from an approximate solution (computed with divergence-free finite elements), we determine a bound for its defect, and a norm bound for the inverse of the linearization at the approximate solution. For the latter, bounds for the essential spectrum and for eigenvalues play a crucial role, especially for the eigenvalues ``close to'' zero. Note that, on an unbounded domain, the only general method for computing the desired norm bound appears to be via eigenvalue bounds. To obtain the desired lower bounds for the eigenvalues below the essential spectrum we use the Rayleigh-Ritz method, a corollary of the Temple-Lehmann theorem and a homotopy method. Finally, if the computer-assisted proof provides the existence of a velocity field, the existence of a corresponding pressure can be obtained by purely analytical techniques. Nevertheless, for a given approximate solution to the pressure our methods provide an error bound (in a dual norm) as well.