KAM quasi-periodic solutions for the dissipative standard map

We present results towards a constructive approach to show the existence of quasiperiodic solutions in non-perturbative regimes of some dissipative systems, called conformally symplectic systems. Finding a quasi-periodic solution of conformally symplectic systems with fixed frequency requires to choose a parameter, called the drift parameter.The first step of the strategy is to establish a very explicit quantitative theorem in an a-posteriori format as in Calleja et al. (2013). A-posteriori theorems show that if we can find an approximate solution of an invariance equation, which is sufficiently approximate with respect to some condition numbers (algebraic expressions of derivatives of the approximate solution and estimates on the derivatives of the map), then there is a true solution.The second step in the strategy is to produce numerically a very accurate solution of the invariance equation (discretizations with 2(18) Fourier coefficients, each one computed with 100 digits of precision).The third step is to compute in a concrete example, the dissipative standard map, the condition numbers and verify numerically the conditions of the theorem in the approximate solutions. For some families which have been studied numerically, the results agree with three figures with the best numerical values. We point out however that the numerical methods developed here work also in examples which have not been accessible to other more conventional methods.The verification of the estimates presented here is not completely rigorous, since we do not control the round-off error, nor the truncation error of several operations in Fourier space. We hope that the positive step taken in this paper will stimulate the complete computer-assisted proof. Making explicit the condition numbers and verifying the conditions (even in an incomplete way) will be valuable for the computation close to breakdown.We make available the approximate solutions, the highly efficient algorithm (quadratic convergence, low storage requirements, low operation count per step) to compute them (incorporating high precision based on the MPFR library) and the routines used to verify the applicability of the theorem.