Rigorous treatment of the averaging process for co-orbital motions in the planetary problem

We develop a rigorous analytical Hamiltonian formalism adapted to the study of the motion of two planets in co-orbital resonance. By constructing a complex domain of holomorphy for the planetary Hamiltonian, we estimate the size of the transformation that maps this Hamiltonian to its first order averaged over one of the fast angles. After having derived an integrable approximation of the averaged problem, we bound the distance between this integrable approximation and the averaged Hamiltonian. This finally allows to prove rigorous theorems on the behavior of co-orbital motions over a finite but large timescale.