标题： 计算机辅助证明在行星动力学模型中存在 KAM 拓扑的$\upsilon$和$\mathbf{b}$ 显示英文标题

标题： Computer-assisted proofs of existence of KAM tori in planetary dynamical models of $\upsilon$-And $\mathbf{b}$

摘要： 我们重新考虑了$\upsilon$-Andromedae 系统中最内层系外行星的轨道动力学问题（即，$\upsilon$-And$\mathbf{b}$）进入一个长期准周期限制哈密顿模型的框架中。 这意味着我们预先设定了在该系外行星系统中预期最大的行星的轨道（即，$\upsilon$-And$\mathbf{c}$和$\upsilon$-And$\mathbf{d}$）。 他们的长期运动的傅里叶分解被引入到描述$\upsilon$-And $\mathbf{b}$在那两颗系外行星引力作用下的轨道动力学的方程中。 通过计算机辅助的过程，我们证明了对应于我们认为非常稳定的轨道运动的KAM环面的存在，根据我们在之前文章中进行的分析和数值探索。 计算机辅助证明成功地应用于两种不同的长期准周期限制哈密顿模型变体，这些变体在相对论修正对$\upsilon$-And $\mathbf{b}$轨道运动的影响方面有所不同，这取决于是否考虑这些修正。 显示英文摘要

摘要： We reconsider the problem of the orbital dynamics of the innermost exoplanet of the $\upsilon$-Andromedae system (i.e., $\upsilon$-And $\mathbf{b}$) into the framework of a Secular Quasi-Periodic Restricted Hamiltonian model. This means that we preassign the orbits of the planets that are expected to be the biggest ones in that extrasolar system (namely, $\upsilon$-And $\mathbf{c}$ and $\upsilon$-And $\mathbf{d}$). The Fourier decompositions of their secular motions are injected in the equations describing the orbital dynamics of $\upsilon$-And $\mathbf{b}$ under the gravitational effects exerted by those two exoplanets. By a computer-assisted procedure, we prove the existence of KAM tori corresponding to orbital motions that we consider to be very robust configurations, according to the analysis and the numerical explorations made in our previous article. The computer-assisted assisted proofs are successfully performed for two variants of the Secular Quasi-Periodic Restricted Hamiltonian model, which differs for what concerns the effects of the relativistic corrections on the orbital motion of $\upsilon$-And $\mathbf{b}$, depending on whether they are considered or not.