How to analytically prove chaos Consider the following map
\begin{align*}
 T \colon \mathbb{R}\times\mathbb{S}^1 \to &  \mathbb{R}\times\mathbb{S}^1 \\
 (x,\theta) \mapsto & \left(\frac{x}{4}+ \sin^2\left(\pi\left(\theta+\frac{x}{2}\right)\right)+0.01, 
 \theta+\frac{3x}{4}+\sin^2\left(\pi\left(\theta+\frac{x}{2}\right)\right)+0.01\right)
 \end{align*}
I have been doing some numerical simulations and it seems this  system presents a chaotic attractor.  Here there is an approximation of the attractor. The colored points are the fixed points of the map.

According by the following result that can be found in the Katok and Hasselblat book

the chaos in this system might be generated by a transverse intersection of stable and unstable manifold of the orange saddle point.

My Question:  How do I check analytically that there is this intersection or how do I prove this map has chaotic behaviour?

Could anyone help me ?
 A: For specific systems at specific parameters, it can often be infeasible to give a pen-and-paper proof of chaos. However there is a rich literature of using computer-assisted-proofs based on interval arithmetic to demonstrate chaos, see for example
Mischaikow, K., & Mrozek, M. (1995). Chaos in the Lorenz equations: a computer-assisted proof. Bulletin of the American Mathematical Society, 32(1), 66-72.
The dynamical system you have looks similar to the Chirikov standard map. The following paper seems quite relevant to the problem you are studying. To quote from their abstract, they "show how interval analysis can be used to calculate rigorously valid enclosures of transversal homoclinic points in discrete dynamical systems."
Neumaier, A., & Rage, T. (1993). Rigorous chaos verification in discrete dynamical systems. Physica D: Nonlinear Phenomena, 67(4), 327-346.
In the intervening three decades there has been much progress and interest in developing computer-assisted-proofs of chaos in dynamical systems. For a more recent resource, I would recommend taking a look at the CAPD library:
Kapela, T., Mrozek, M., Wilczak, D., & Zgliczyński, P. (2021). CAPD:: DynSys: a flexible C++ toolbox for rigorous numerical analysis of dynamical systems. Communications in Nonlinear Science and Numerical Simulation, 101, 105578.
