Rigorous existence results for the Euler or Navier-Stokes equations from a posteriori analysis of approximate solutions

This communication presents results from joint work with Carlo Morosi (Politecnico di Milano) and Mario Pernici (Istituto Nazionale di Fisica Nucleare, Sezione di Milano). The Cauchy problem is considered for the incompressible Euler or Navier-Stokes (NS) equations on a d dimensional torus T^d, in the framework of the Sobolev spaces H^n(T^d)(n > d/2 + 1). In papers [Morosi and Pizzocchero: Nonlinear Analysis, 2012, Commun. Pure Appl. Anal. 2012, Appl. Math. Lett. 2013] (partly inspired by, or related to [Chernyshenko, Constantin, Robinson and Titi, J.Math. Phys. 2007],[Morosi and Pizzocchero: Rev. Math. Phys. 2008, Nonlinear Analysis 2011]) an approach has been developed to obtain rigorous and fully quantitative results on the exact solution u of the Euler or NS Cauchy problem from the a posteriori analysis of any approximate solution u_a. This approach allows to derive estimates on the interval of existence [0,T) of the exact solution u, and on the Sobolev distance between the exact and the approximate solution. The latter estimate has the form || u(t)-u_a(t) ||_n <= R_n(t) where R_n(t) is a real, nonnegative function of time t, obtained solving a differential ``control inequality''. In particular, the exact solution u of the Cauchy problem is granted to be global in time if the control inequality has a global solution R_n : [0,+\infinity) -> [0,+\infinity). In the present communication, the above general setting is exemplified working in dimension d=3 with simple initial data, such as the Behr-Necas-Wu vortex [ESAIM:M2AN 2001]. The approximate solutions in these examples are of the following types: (i) Galerkin solutions for Euler or NS equations (corresponding to suitable sets of Fourier modes) [Morosi and Pizzocchero, Nonlinear Analysis 2012]; (ii) Large order Taylor expansions in time for the Euler equations [Morosi, Pernici and Pizzocchero, ESAIM:M2AN 2013][Morosi, Pernici and Pizzocchero, submitted]; (iii) Large order expansions in the Reynolds number for the NS equations [Morosi and Pizzocchero, arXiv:1304.2972][Morosi, Pernici and Pizzocchero, in preparation]. Under specific conditions (on the datum and/or the viscosity), the approach based on (i) or (iii) allows to infer the global existence of the exact solution u for the NS Cauchy problem. In cases (ii)(iii), the construction of the approximate solution and its a posteriori analysis is performed using tools for automatic symbolic computation, finally yielding ``computer assisted proofs'' of existence and regularity for the Euler or NS equations.